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:

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:

inclusion super-rules

which can be respectively read as «if x0Y assuming that x0X, then XY» and «knowing that x0X, if we can deduce a proposition P from the fact that x0Y, then we can deduce P from the fact that XY». 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))


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

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)


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


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

partial proof tree

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 ' ' ':'`

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

You can now run it:


Example files are avalaible in the tests directory. Have fun !

Commands summary

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

Toplevel mode

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

Proof mode

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)