A sequent calculus and a theorem prover for standard conditional logics
Nicola Olivetti, Gian Luca Pozzato, Camilla B. Schwind · ACM Transactions on Computational Logic · 2007
In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a theorem prover in Prolog for these calculi.