next up previous contents
Next: Installing NDL Up: Natural Deduction Language Previous: Contents   Contents

What is NDL?

NDL (Natural Deduction Language) is a formal language for expressing natural deduction (``Fitch-style'') proofs in first-order logic with equality. The proofs are machine-checkable. NDL is a ``formal language'' in that it has a formal syntax, and, more importantly, a formal semantics. The semantics are given in Plotkin's SOS+1.1 style and are centered around the notion of assumption bases. Assumption-base semantics is the hallmark of a family of proof languages known as DPLs (Denotational Proof Languges). NDL is a simple DPL+1.2 for first-order logic. An assumption base is just a set of premises--a set of statements that we take for granted for the purposes of the proof. This is traditionally known in logic as a ``context,'' a notion that has been around for a while, in particular in connection with sequent systems, where the basic unit of inference is a pair \bgroup\color{red}$(\mbox{$\beta$},F)$\egroup consisting of a context and a conclusion. What is novel about DPLs is that the formal meaning--denotation--of a DPL proof is specified relative to a given assumption base (context). That is, the meaning of a DPL proof is a function over assumption bases, in the same way that in denotational semantics the meaning of an imperative program is a function over stores. This is a fecund viewpoint that is particularly conducive to giving a rigorous semantics to Fitch-style natural deduction. Unlike sequent systems, where the manipulation of the context is explicit and burdens the user, the manipulation and threading of the context in systems such as NDL is implicit and relegated to the underlying semantics--again, much as the manipulation and threading of the store in imperative languages is hidden from the user. The key idea is that if a DPL proof is sound, then its meaning is the conclusion established by the proof; if the proof is unsound, then its meaning is error. To obtain that meaning, we evaluate the proof in some given assumption base and in accordance with the formal semantics of the language. Evaluation will either produce the advertised conclusion, which will verify that the proof is sound, or else it will generate an error, which will indicate that the proof is unsound. Thus in DPLs evaluation is tantamount to proof checking. In NDL, in particular, evaluation (and hence proof-checking) is guaranteed to terminate in quadratic time in the length of the proof (in the worst case). This tutorial pertains to a graphical Java-based implementation of NDL. Versions are available for Windows, Linux, and the Mac operating systems. They can be obtained from the NDL web page:

\begin{displaymath}\bgroup\color{red}\mbox{\tt www.cag.lcs.mit.edu/~kostas/dpls/ndl}\egroup\end{displaymath}

and distributed in accordance with GPL, the copyright licence of GNU.
next up previous contents
Next: Installing NDL Up: Natural Deduction Language Previous: Contents   Contents
2004-08-06