A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
<|reference_start|>A Sequent Calculus and a Theorem Prover for Standard Conditional Logics: 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.<|reference_end|>
@article{olivetti2004a,
    title={A Sequent Calculus and a Theorem Prover for Standard Conditional Logics},
    author={Nicola Olivetti, Gian Luca Pozzato, Camilla Schwind},
    journal={arXiv preprint arXiv:cs/0407064},
    year={2004},
    archivePrefix={arXiv},
    eprint={cs/0407064},
    primaryClass={cs.LO cs.AI}
}