NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics

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/