NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics

ABSTRACT. In this paper 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. NESCOND also deals with the flat fragment (i.e., without nested conditionals) of the conditional logic CK+CSO+ID, which corresponds to the cumulative logic C introduced by Kraus, Lehmann and Magidor. NESCOND is inspired to the methodology of leanTAP and it is implemented in Prolog. The paper also shows some experimental results, witnessing that the performances of NESCOND are promising. NESCOND is available at http://www.di.unito.it/~pozzato/nescond/