A proof assistant for superdeduction

Lemuridae is a proof assistant allowing the building of proofs in the extendible sequent calculus, a.k.a. superdeduction for the sequent calculus. It is written in Tom and features super-rules derivation with focussing as well as some basic automatic tactics. The correctness is ensured by a tiny kernel checking the generated proof trees.

Superdeduction [pdf] is an extension of logical deduction systems consisting in canonically adding ad hoc deduction rules translating axiomatic theories. This has several advantages:

- Proofs are far more readable and close to the "classical" mathematical reasonning.
- As in deduction modulo [DHK-TPM-2003, pdf], purely computational parts of the proofs are separated from the logical arguments. Unlike deduction modulo, the interactive building of such proofs is rather intuitive.
- Axioms are expressed via rewrite systems. Checking some criteria on these systems automatically ensures consistancy of the encoded theory.
- Automated proof search may speed up in such systems since some systematic parts of the proofs are "compiled" into super deduction rules.

Superdeduction applied to natural deduction was first introduced by Benjamin Wack in its phd thesis [pdf]. It has been ported to sequent calculus and improved by Paul Brauner and Clément Houtmann in their master thesis [brauner, ps] [houtmann, ps].

We start by adding some definitions (axioms), which are automatically translated into super-rules:

```
brauner@orain:~/lemu$ ./lemu
> rule subset(X,Y) -> \Ax.(in(x,X) => in(x,Y)).
The new deduction rules are :
x0 in X |- x0 in Y
------------------ (x0 not in FV)
|- subset(X, Y)
|- x0 in X x0 in Y |-
--------------------------
subset(X, Y) |-
>
```

It means that the rewrite rule X ⊆ Y → ∀ x ( x ∈ X ⇒ x ∈ Y ) has been translated into the two additional following deduction rules:

which can be respectively read as «if x_{0} ∈ Y assuming that x_{0} ∈ X, then X ⊆ Y» and «knowing that x_{0} ∈ X, if we can deduce a proposition P from the fact that x_{0} ∈ Y, then we can deduce P from the fact that X ⊆ Y». Let us add the definition of the empty set (x ∈ ø → ⊥) too:

```
> rule in(x,emptyset()) -> \B .
The new deduction rules are :
|- False
-------------------
|- x in emptyset()
-------------------
x in emptyset() |-
>
```

Let us now prove a very complicated theorem, that is the empty set is included in every set:

```
> proof emptySetInAll: \A A.subset(emptyset(),A).
Open goals :
|- forall A.(subset(emptyset(), A))
-----------
*c1: forall A.(subset(emptyset(), A))
proof>
```

As in traditional theorem proving assistants, the environement is divided into three parts:

- The list of the open goals - one sequent here;
- The hypothesis for the current goal - none here, with a classical proof assistant, the former definitions would be displayed there;
- The list of the conclusions for the current goals (as we work with classical sequent calculus, there can be many) - here we only have c1.

The star means that we are focused on c1.

The first deduction step consists in introducing the universal quantifier:

```
proof> intro.
Open goals :
|- subset(emptyset(), A0)
-----------
*c1: subset(emptyset(), A0)
proof>
```

We are now in an odd situation: the «head connector» appears to be a predicate symbol and we have no related hypothesis to go on with the proof. However, remember we have derived new deduction rules at the begining of the session. Let us ask lemu which of them are applicable:

```
proof> showrules.
- rule 0 :
x0 in X |- x0 in Y
------------------ (x0 not in FV)
|- subset(X, Y)
```

Since there is only one, we just type `rule`

to apply it to the focused proposition:

```
proof> rule.
Open goals :
x0 in emptyset() |- x0 in A0
h1: x0 in emptyset()
-----------
*c1: x0 in A0
proof>
```

At any moment, we can see how the current proof tree looks like by typing `display`

.

We finish to prove the proposition by focusing the h1 hypothesis and by using an other super-rule:

```
proof> focus h1.
Open goals :
x0 in emptyset() |- x0 in A0
*h1: x0 in emptyset()
-----------
c1: x0 in A0
proof> rule.
emptySetInAll proved.
```

Lemuridae is available in the Tom subversion repository, under the path `applications/lemuridae`

.
You can get it through anonymous acces:

`svn checkout svn://scm.gforge.inria.fr/svn/tom/jtom/trunk jtom`

Then, you have to compile Tom SVN to get lemu working. After checking for the presence of java 5.0 and ant on your system, type the following commands:

```
cd jtom
./build.sh stable
./build.sh src.dist
```

Now add the follwing lines into your `.bashrc`

config file (please adapt to your shell if you're not using bash), where `/path/to/jtom`

represents the directory created by the subversion checkout:

```
export TOM_HOME=/path/to/jtom/src/dist
export PATH=$TOM_HOME/bin:$PATH
TOM_LIB=`echo ${TOM_HOME}/lib/*.jar | tr ' ' ':'`
export CLASSPATH=${TOM_LIB}:${CLASSPATH}
```

Read your `.bashrc`

again (by launching a new shell for instance). Now you have a fully working tom installation, don't hesitate to play with ! The last step consists in compiling lemuridae itself:

```
cd applications/lemuridae
ant
```

You can now run it:

```
./lemu
>
```

Example files are avalaible in the `tests`

directory. Have fun !

The available commands vary depending on the mode. There are two modes:

- The
*toplevel*mode, which allows to declare rules, axioms and to manipulate proofs; - The
*proof*mode, where the programm is waiting for tactics.

`proof <name> : <proposition> .` | enter proof mode to prove the proposition |

`display <name> .` | display the proof tree of the proof name |

`rule <atomic_proposition> -> <proposition> .` | declare a rewrite rule on propositions (an axiom) |

`termrule <term> -> <term> .` | declare a rewrite rule on terms |

`reduce term <term> .` | normalizes term wrt. the term rewriting system |

`reduce proposition <prop> .` | normalirzes prop wrt. the proposition rewriting system |

`quit.` | exit lemu |

`undo.` | cancel the last step (infinite undo) |

`next.` | work on the next sub-goal |

`display.` | display the partial proof tree of the current proof |

`focus <label>.` | focus on the hypothesis/conclusion denoted by label |

`showrules.` | show applicable super-rules |

`rule <n>.` | apply rule number n |

`rule.` | if there is only one applicable super-rule then apply it |

`intro.` | introduces the head connector of the focused proposition |

`intros.` | recursively introduces all trivial connectors |

`axiom.` | apply the axiom inference rule |

`duplicate.` | apply a contraction rule on the focused proposition |

`remove.` | apply a weakening rule on the focussing proposition |

`auto.` | dummy automated proof-search strategy : stops at variable instanciation |

`cut <proposition>.` | cuts the sequent on the proposition |

`reduce.` | normalize all terms of the sequent (potential infinite loop) |