We present NESCOND, a theorem prover for normal conditional logics. NESCOND implements some recently introduced NESted sequent calculi for propositional CONDitional logics CK and some of its significant extensions with axioms ID, MP and CEM. It also deals with the flat fragment of CK+CSO+ID, which corresponds to the logic C introduced by Kraus, Lehmann and Magidor. NESCOND is inspired by the methodology of leanT(A)P and it is implemented in Prolog. The paper shows some experimental results, witnessing that the performances of NESCOND are promising. The program NESCOND, as well as all the Prolog source files, are available at http://www.di.unito.it/similar to pozzato/nescond/
NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics
POZZATO, GIAN LUCA
2014-01-01
Abstract
We present NESCOND, a theorem prover for normal conditional logics. NESCOND implements some recently introduced NESted sequent calculi for propositional CONDitional logics CK and some of its significant extensions with axioms ID, MP and CEM. It also deals with the flat fragment of CK+CSO+ID, which corresponds to the logic C introduced by Kraus, Lehmann and Magidor. NESCOND is inspired by the methodology of leanT(A)P and it is implemented in Prolog. The paper shows some experimental results, witnessing that the performances of NESCOND are promising. The program NESCOND, as well as all the Prolog source files, are available at http://www.di.unito.it/similar to pozzato/nescond/File | Dimensione | Formato | |
---|---|---|---|
IJCAR2014 proofs.pdf
Accesso aperto
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
379.94 kB
Formato
Adobe PDF
|
379.94 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.