An Alloy Model for Derivations by Natural Deduction

Alloy is a “lightweight formal methods” tool that has been used primarily to explore abstract software designs. “Alloy” refers to both a logic (which combines elements of first order logic and relational calculus) and a tool for analyzing models specified in that logic. The language is in fact quite general and people have found a wide range of applications of the tool — I’m sure many that the original developers (led by Daniel Jackson) never envisioned.

In this post I will show an Alloy model I made for my course Logic in Computer Science. We spend a good bit of time in the course doing derivations (formal proofs) by Natural Deduction (ND), first for Propositional Logic (PL), then for First Order Logic. Here are the rules of ND for PL as presented in Rigorous Software Development by Almeida, Frade, Pinto and de Sousa, Springer, 2011:

A judgment in this logic is a sequent of the form \(\Gamma\vdash A\), where \(\Gamma\) is a set of (propositional) formulas and \(A\) is a formula. The rules specify when you can conclude new judgments from old. For example, rule (Ax) says that one can always conclude \(\Gamma\cup\{A\}\vdash A\) for any set \(\Gamma\) and formula \(A\) (\(\Gamma, A\) being shorthand for the set \(\Gamma\cup\{A\}\)). Rule \((\textrm{I}_\neg)\) says that if one has derived \(\Gamma,A\vdash\bot\) then one may conclude \(\Gamma\vdash\neg A\). Here is a derivation of the “law of the excluded middle”, \(\emptyset\vdash p\vee\neg p\):

\begin{array}{rrcll} 0. & \neg(p\vee\neg p), \neg p & \vdash & \neg p & (\textrm{Ax}) \\ 1. & \neg(p\vee\neg p), \neg p & \vdash & p\vee\neg p & (\textrm{I}_{\vee2})0\\ 2. & \neg(p\vee\neg p), \neg p & \vdash & \neg(p\vee\neg p) & (\textrm{Ax})\\ 3. & \neg(p\vee\neg p), \neg p & \vdash & \bot & (\textrm{E}_\neg)1,2\\ 4. & \neg(p\vee\neg p) & \vdash & p & (\textrm{RAA})3\\ 5. & \neg(p\vee\neg p) & \vdash & \neg(p\vee\neg p) & (\textrm{Ax})\\ 6. & \neg(p\vee\neg p) & \vdash & p\vee\neg p & (\textrm{I}_{\vee1})4\\ 7. & \neg(p\vee\neg p) & \vdash & \bot & (\textrm{E}_\neg)6,5\\ 8. & & \vdash & p\vee\neg p & (\textrm{RAA})7 \end{array}

The following Alloy model specifies an ND derivation for PL. Using this model, the Alloy Analyzer can automatically find a derivation for a given sequent. It is a good demonstration of the expressiveness of the Alloy logic. In 218 lines (including comments), the syntax of PL, derivations, and the rules of ND are fully specified, as well as several examples:

The model defines the syntax for a propositional logic formula, and then defines the structure of a derivation, which is a recursive (tree-like) structure. Each node is the application of one of 12 rules, has some number (\(\leq 3\)) of children (premises, or sub-derivations), and a conclusion, which is a sequent of the form \(S\vdash f\), where \(S\) is a set of formulas (the antecedents) and \(f\) is a formula (the consequent). Then there is a series of examples where I describe the desired sequent and ask Alloy to find a derivation of it.

From the Alloy Analyzer menu, if we select to execute the “run LEM…” command, the result, after a few seconds, is an instance of the model. The instance can be viewed in Alloy’s Table view mode. The first table shows the Formulas. In addition to the atomic formulas False (\(\bot\)) and Prop0 (\(p\)), the following three compound formulas appear:

These represent, in order: \(\neg(p\vee\neg p)\), \(\neg p\), and \(p\vee\neg p\). Now here is the derivation, exactly as it appears in Alloy’s Table view:

which is exactly the derivation one would write by hand and is shown above.

Notice that we never had to specify any algorithm to find derivations. Rather, we just had to tell Alloy what a derivation looks like, and Alloy—and the PLingeling SAT solver—do the hard work of finding something matching our description.

One thought on “An Alloy Model for Derivations by Natural Deduction

  1. Nice! I am constantly surprised by all the novel applications of Alloy people come up with.
    Do you think this could be extended to a model for ND for First Order Logic? I imagine the SAT problems would really start to blow up…

Leave a Reply