Abstract
We propose a new method for using recurrent schematizations in Theorem Proving. We provide techniques for detecting cycles in proofs (via proof generalization), and we show how to take advantage of the expressive power of schematizations in order to avoid generating such cycles explicitly. This may shorten proofs and avoid divergence in some cases. These techniques are more general than existing ones, and unlike them, they can be used with any kind of proof procedure (using tableaux-based approaches as well as resolution-based ones).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
H. Chen and J. Hsiang. Logic programming with recurrence domains. In Automata, Languages and Programming (ICALP’91), pages 20–34. Springer, LNCS 510, 1991.
H. Chen, J. Hsiang, and H. Kong. On finite representations of infinite sequences of terms. In Conditional and Typed Rewriting Systems, 2nd International Workshop, pages 100–114. Springer, LNCS 516, June 1990.
H. Comon. On unification of terms with integer exponents. Mathematical System Theory, 28:67–88, 1995.
M. Hermann. Divergence des systèmes de réécriture et schématisation des ensembles infinis de termes. Habilitation, Université de Nancy I, and CRIN-CNRS Inria-Lorraine, Nancy, France, March 1994.
M. Hermann and R. Galbavý. Unification of Infinite Sets of Terms schematized by Primal Grammars. Theorical Computer Science, 176(1-2):111–158, 1997.
S. Klingenbeck. Counter Examples in Semantic Tableaux. PhD thesis, University of Karlsruhe, 1996.
R. Manthey and F. Bry. SATCHMO: A theorem prover implemented in Prolog. In Proc. of CADE-9, pages 415–434. Springer, LNCS 310, 1988.
N. Peltier. Increasing the capabilities of model building by constraint solving with terms with integer exponents. Journal of Symbolic Computation, 24:59–101, 1997.
N. Peltier. Using Term Schematizations in Automated Deduction. Research Report. Available on http://www-leibniz.imag.fr/ATINF/Nicolas.Peltier/, 2001.
G. Salzer. Unification of Meta-Terms. PhD thesis, Technische Universität Wien., 1991.
G. Salzer. The unification of infinite sets of terms and its applications. In Logic Programming and Automated Reasoning (LPAR’92), pages 409–429. Springer, LNAI 624, July 1992.
G. Salzer. Primal grammar and unification modulo a binary clause. In Proc. of CADE-12, pages 72–86. Springer, 1994. LNAI 814.
F. Stolzenburg. Loop-detection in hyper-tableaux by powerful model generation. Journal of Universal Computer Science, 5(3):135–155, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Peltier, N. (2001). A General Method for Using Schematizations in Automated Deduction. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_48
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive