Logic Programming and Automated Reasoning group's - Dipartimento di Informatica


DIPARTIMENTO DI INFORMATICA Università di Torino

Gian Luca Pozzato and Nicola Olivetti

CondLean 3.2: a Theorem Prover for Conditional Logics

Conditional logics have a long history, and recently they have found several applications in artificial intelligence, such as deductive databases, nonmonotonic reasoning, belief revision. CondLean 3.2 is a theorem prover implementing some sequent calculi for these logics. It is written in SICStus Prolog and also comprises a GUI written in Java. In this page you will find all you need to run and use CondLean 3.2. If you need some help, please contact: pozzato[at]di.unito.it or consult the user manual.

Supported conditional logics and SICStus Prolog source code

Download the program CondLean 3.2

GoalDuck: a goal-directed theorem prover for conditional logic CK

Supported conditional logics and SICStus Prolog source code

CondLean 3.2 implements calculi for the basic normal conditional system CK and for the some extensions of it characterized by the following axioms:

*Axioms for extensions of CK*
System	Axiom
ID	A => A
MP	(A => B) -> ( A -> B)
CS	(A & B) -> (A => B)
CEM	(A => B) v (A => ~B)

For each system of conditional logics, CondLean implements three different versions of theorem prover: constant labels version, free-variables version, and heuristic version.
The list of the conditional systems supported by CondLean 3.2 and the corresponding SICStus Prolog source code is reported in the folowing tables (all combinations of the above axioms are available, with the exception of CK+CEM+MP and CK+CEM+ID+MP, notice that CS can be derived by CEM+MP):

Supported systems and SICtus Prolog source code
constant labels versions
Conditional logic	SICStus Prolog source code
CK	code
CK+ID	code
CK+MP	code
CK+CS	code
CK+CEM	code
CK+ID+MP	code
CK+CS+ID	code
CK+CEM+ID	code
CK+CS+MP	code
CK+CS+CEM	code
CK+CS+ID+MP	code
CK+CEM+CS+ID	code

Supported systems and SICtus Prolog source code
free-variables versions
Conditional logic	SICStus Prolog source code
CK	code
CK+ID	code
CK+MP	code
CK+CS	code
CK+CEM	code
CK+ID+MP	code
CK+CS+ID	code
CK+CEM+ID	code
CK+CS+MP	code
CK+CS+CEM	code
CK+CS+ID+MP	code
CK+CEM+CS+ID	code

Supported systems and SICtus Prolog source code
heuristic versions
Conditional logic	SICStus Prolog source code
CK	code
CK+ID	code
CK+MP	code
CK+CS	code
CK+CEM	code
CK+ID+MP	code
CK+CS+ID	code
CK+CEM+ID	code
CK+CS+MP	code
CK+CS+CEM	code
CK+CS+ID+MP	code
CK+CEM+CS+ID	code

SICStus Prolog source code of an alternative implementation for conditional logic CK following the "lean" methodology in a more rigorous manner: leanCK

Download the program CondLean 3.2

CondLean 3.2 comprises a graphical interface written in Java. One can prove the validity of a sequent by putting it into the text fields and then clicking a button. If the sequent is valid, CondLean 3.2 offers three different alternatives: 1. to display the proof tree of the sequent in a special window; 2. to build a latex file containing the same proof; 3. to display some statistics of the proof.

CondLean 3.2 (zip file, 4,10 MB)

How to install CondLean 3.2 running Windows:

1. Extract condlean3.2.zip into a folder, for instance C:\Programs\CondLean 3.2;
2. Open file condlean3.2.bat with a text editor;
3. Replace C:\j2sdk1.4.2_13\bin with your java path;
4. Replace C:\Programmi\SICStus Prolog 3.12.2 with your SICStus Prolog path;
5. Replace C:\CondLean 3.2 with the installation directory (in the above example, C:\Programs\CondLean 3.2);
6. Run condlean3.2.bat

Note: remember to copy files prooftree.sty and mem3.cls into the directory where latex output files are saved before compiling .tex files.

GoalDuck: a goal-directed theorem prover for conditional logic CK

We have also implemented a goal-directed proof procedure for the basic normal conditional logic CK. This goal-directed theorem prover is called GoalDuck. Here below is the link to its SICStus Prolog source code.

GoalDuck source code

Back to Gian Luca Pozzato's home page