A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
Logic in Computer Science
2007-05-23 v1 Artificial Intelligence
Abstract
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.
Keywords
Cite
@article{arxiv.cs/0407064,
title = {A Sequent Calculus and a Theorem Prover for Standard Conditional Logics},
author = {Nicola Olivetti and Gian Luca Pozzato and Camilla Schwind},
journal= {arXiv preprint arXiv:cs/0407064},
year = {2007}
}
Comments
45 pages with 2 figures, uses prooftree.sty