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 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): 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.
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.
Back to Gian Luca Pozzato's home page |