In this paper we focus on theorem proving for conditional logics. First, we give a detailed description of CondLean, a theorem prover for some standard conditional logics. CondLean is a SICStus Prolog implementation of some labelled sequent calculi for conditional logics recently introduced. It is inspired to the so called “lean” methodology, even if it does not fit this style in a rigorous manner. CondLean also comprises a graphical interface written in Java. Furthermore, we introduce a goal-directed proof search mechanism, derived from the above mentioned sequent calculi based on the notion of uniform proofs. Finally, we describe GOALDUCK, a simple SICStus Prolog implementation of the goal-directed calculus mentioned here above.
Theorem Proving for Conditional Logics: CondLean and GoalDuck
POZZATO, GIAN LUCA
2008-01-01
Abstract
In this paper we focus on theorem proving for conditional logics. First, we give a detailed description of CondLean, a theorem prover for some standard conditional logics. CondLean is a SICStus Prolog implementation of some labelled sequent calculi for conditional logics recently introduced. It is inspired to the so called “lean” methodology, even if it does not fit this style in a rigorous manner. CondLean also comprises a graphical interface written in Java. Furthermore, we introduce a goal-directed proof search mechanism, derived from the above mentioned sequent calculi based on the notion of uniform proofs. Finally, we describe GOALDUCK, a simple SICStus Prolog implementation of the goal-directed calculus mentioned here above.File | Dimensione | Formato | |
---|---|---|---|
jancl.18.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
577.14 kB
Formato
Adobe PDF
|
577.14 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.