A Sequent Calculus and Theorem Prover for Standard Conditional Logics

Nicolas Olivetti , Gian Luca Pozzato , Camilla Schwind (1)

1 MAP - Modèles et simulation pour l'architecture, l'urbanisme et le paysage

In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics, namely CK, CK+ID, CK+MP and CK+MP+ID. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also present CondLean, a theorem prover for these logics implementing SeqS calculi written in SICStus Prolog.

Mots clés: Sequent Calculus

Domaines: Architecture, aménagement de l'espace

Nicolas Olivetti, Gian Luca Pozzato, Camilla Schwind. A Sequent Calculus and Theorem Prover for Standard Conditional Logics. The Computing Research Repository, 2004. ⟨halshs-00261169⟩