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.