Lemuridae
A proof assistant for superdeduction

Description

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

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].

The assistant

Let's begin with an example

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₀ ∈ Y assuming that x₀ ∈ X, then X ⊆ Y» and «knowing that x₀ ∈ X, if we can deduce a proposition P from the fact that x₀ ∈ 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.

Downloading and Installing Lemu

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 !

Commands summary

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.

Toplevel mode

Proof mode