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 𝗅𝖾𝖺𝗇T 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/ pozzato/nescond/.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Lellmann, Björn: From input/output logics to conditional logics via sequents -- with provers (2021)
- Girlando, Marianna; Lellmann, Björn; Olivetti, Nicola; Pozzato, Gian Luca; Vitalis, Quentin: VINTE: an implementation of internal calculi for lewis’ logics of counterfactual reasoning (2017)
- Ramanayake, Revantha: Inducing syntactic cut-elimination for indexed nested sequents (2016)
- Zohar, Yoni; Zamansky, Anna: Gen2sat: an automated tool for deciding derivability in analytic pure sequent calculi (2016)
- Olivetti, Nicola; Pozzato, Gian Luca: NESCOND: an implementation of nested sequent calculi for conditional logics (2014)