In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a theorem prover in Prolog for these calculi.
A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
POZZATO, GIAN LUCA;
2007-01-01
Abstract
In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a theorem prover in Prolog for these calculi.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
ACMtoclConditionalLogics.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
660.18 kB
Formato
Adobe PDF
|
660.18 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.
