Abstract
In application areas like formal software verification or in connection with lemma use, the success of automated theorem provers strongly depends on their ability to choose from a huge number of given axioms only some relevant ones. We present a new technique for deleting irrelevant clauses for model elimination proof procedures which is based on the use of abstractions. We analyze general conditions under which abstractions are well-suited for choosing useful clauses and investigate whether certain abstractions are applicable. So-called symbol abstractions are further examined in a case study which, e.g., introduces new techniques for the automatic generation of abstractions. We evaluate our techniques by means of experiments performed with the prover Setheo.
This is a preview of subscription content, log in via an institution to check access.
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
D. Barker-Plummer. Gazing: An Approach to the Problem of Definition and Lemma Use. JAR, 8:311–344, 1992.
M. Fuchs. Abstraction-Based Relevancy Testing for Model Elimination. AR-Report AR-98-5, 1998, Technische Universität München, Institut für Informatik, 1998.
M. Fuchs. Relevancy-Based Lemma Selection for Model Elimination using Lazy Tableaux Enumeration. In Proc. ECAI-98, pages 346–350, 1998.
M. Fuchs. System Description: Similarity-Based Lemma Generation for Model Elimination. In Proceedings of CADE-15, pages 33–37, 1998.
F. Giunchiglia and T. Walsh. A Theory of Abstraction. AI, 56(2-3):323–390, 1992.
R. Korf. Macro-Operators: A Weak Method for Learning. AI, 26:35–77, 1985.
R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. JAR, 13:297–337, 1994.
D.W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.
M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. The Model Elimination Provers SETHEO and E-SETHEO. JAR, 18(2), 1997.
D.A. Plaisted. Theorem Proving with Abstraction. AI, 16:47–108, 1981.
D.A. Plaisted. Abstraction Using Generalization Functions. In Proceedings of CADE-8, pages 365–376, 1986.
D.A. Plaisted. Mechanical Theorem Proving. In Formal Techniques in Artificial Intelligence. Elsevier Science Publisher B.V., 1990.
J. Schumann. Delta-a bottom-up preprocessor for top-down theorem provers. system abstract. In Proceedings of CADE-12, 1994.
M.E. Stickel. A prolog technology theorem prover: Implementation by an extended prolog compiler. JAR, 4:353–380, 1988.
J.D. Tenenberg. Preserving Consistency across Abstraction Mappings. In Proceedings of IJCAI-87, pages 1011–1014, 1987.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fuchs, M., Fuchs, D. (1999). Abstraction-Based Relevancy Testing for Model Elimination. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_31
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive