Abstract
We discuss an adaptation of the technique of saturation up to redundancy, as introduced by Bachmair and Ganzinger [1], to tableau and sequent calculi for classical first-order logic. This technique can be used to easily show the completeness of optimized calculi that contain destructive rules e.g. for simplification, rewriting with equalities, etc., which is not easily done with a standard Hintikka-style completeness proof. The notions are first introduced for Smullyan-style ground tableaux, and then extended to constrained formula free-variable tableaux.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2, vol. I, pp. 19–99. Elsevier Science B.V., Amsterdam (2001)
Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation 121(2), 172–192 (1995)
Cantone, D., Zarba, C.G.: A tableau calculus for integrating first-order reasoning with elementary set theory reasoning. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 143–159. Springer, Heidelberg (2000)
Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)
Giese, M.: A model generation style completeness proof for constraint tableaux with superposition. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS, vol. 2381, pp. 130–144. Springer, Heidelberg (2002)
Giese, M.: Simplification rules for constrained formula tableaux. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol. 2796, pp. 65–80. Springer, Heidelberg (2003)
Giese, M.: A calculus for type predicates and type coercion. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 123–137. Springer, Heidelberg (2005)
Smullyan, R.M.: First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete, vol. 43. Springer, Heidelberg (1968)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giese, M. (2006). Saturation Up to Redundancy for Tableau and Sequent Calculi. In: Hermann, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2006. Lecture Notes in Computer Science(), vol 4246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916277_13
Download citation
DOI: https://doi.org/10.1007/11916277_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48281-9
Online ISBN: 978-3-540-48282-6
eBook Packages: Computer ScienceComputer Science (R0)