Abstract
In this paper, we present a further liberalization of the δ-rule in free variable semantic tableaux. It is effective in that (1) it is both a natural and intuitive liberalization, and (2) can reduce the proof size non elementarily as compared to previous versions of the δ-rule.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Baaz, C.G. Fermüller. Non-elementary speedups between different versions of tableaux. In 4th International Workshop, TABLEAUX’95 LNCS n. 918, 1995.
B. Beckert, R. Hähnle and P. Schmitt. The even more liberalized δ-rule in free variable semantic tableaux. In Computational Logic and Proof Theory, Proceedings of the 3rd Kurt Gödel Colloquium, Brno, August 1993. Springer, LNCS 713, pp. 108–119.
D. Cantone, M. Nicolosi Asmundo and E. Omodeo. Global Skolemization with grouped quantifiers. In Proceedings of APPIA-GULP PRODE’97: Joint Conference on Declarative Programming, pp. 405–413, 1997.
M.D. Davis and R. Fechter. A free variable version of the first-order predicate calculus. Journal of Logic and Computation, 1(14):431–451, 1991.
M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, New York, 1990.
R. Hähnle and P. Schmitt. The liberalized δ-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2):211–221, 1994.
R. Smullyan. First-Order Logic. Springer, New York, 1968.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cantone, D., Asmundo, M.N. (2000). A Further and Effective Liberalization of the δ-Rule in Free Variable Semantic Tableaux. In: Caferra, R., Salzer, G. (eds) Automated Deduction in Classical and Non-Classical Logics. FTP 1998. Lecture Notes in Computer Science(), vol 1761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46508-1_7
Download citation
DOI: https://doi.org/10.1007/3-540-46508-1_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67190-9
Online ISBN: 978-3-540-46508-9
eBook Packages: Springer Book Archive