NDL

NDL ("Natural Deduction Language") is a denotational proof language for a Fitch-style natural-deduction formulation of classical first-order logic, developed at MIT by Konstantine Arkoudas. The implementation of NDL that appears on this Web site is essentially a graphical-based proof checker: The user types a proof and then presses "Evaluate" to check the proof. This will either produce the conclusion of the proof, which will verify that the proof is sound, or else it will generate an error message, which means that the proof was unsound. The message will point out exactly what the error was and where it occurred.

Proof checking is guaranteed to terminate quickly (this particular implementation has quadratic worst-case complexity in the length of the proof, but a slightly more sophisticated implementation can achieve n log n worst-case time and linear average-case time). The program can also be run from the command line, which is convenient if NDL is used as a proof checker by another program that invokes NDL as an external process. The implementation along with the syntax and semantics of NDL are thoroughly described in the tutorial below. To install NDL, download the appropriate distribution and follow the installation instructions given below:

Automatic proof simplification

An algorithm has been developed and implemented that can simplify NDL proofs, sometimes resulting in dramatic size reductions. The algorithm is of practical interest because many first-order-logic proofs that are produced mechanically (e.g. by automated theorem provers) contain redundancies and superfluous "detours." This paper (recently accepted for publication in JAR, the Journal of Automated Reasoning) treats the topic extensively. The code that implements the simplification algorithm can be found here. Feel free to email Konstantine Arkoudas (konstantine "at" alum "dot" mit "dot" edu) if you have any questions.