Abstract
We present a general framework for developing search heuristics for automated theorem provers. This framework allows for the construction of heuristics that are on the one hand able to replay (parts of) a given proof found in the past but are on the other hand flexible enough to deviate from the given proof path in order to solve similar proof problems. We substantiate the abstract framework by the presentation of three distinct techniques for learning search heuristics based on so-called features. We demonstrate the usefulness of these techniques in the area of equational deduction. Comparisons with the renowned theorem prover OTTER validate the applicability and strength of our approach.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Avenhaus, J.; Denzinger, J.; Fuchs, Matt.: DISCOUNT: A system for distributed equational deduction, Proc. 6th RTA, Kaiserslautern, FRG, 1995, LNCS 914, pp. 397–402.
Brock, B.; Cooper, S.; Pierce, W.: Analogical reasoning and proof discovery, Proc. CADE 9, Argonne, IL, USA, 1988, LNCS 310, pp. 454–468.
Bachmair, L.; Dershowitz, N.; Plaisted, D.A.: Completion without Failure, Coll. on the Resolution of Equations in Algebraic Structures, Austin (1987), Academic Press, 1989.
Cover, T.M.; Hart P.E.: Nearest Neighbor pattern classification, IEEE, Transactions on Information Theory 13, pp. 21–27, 1967.
Fuchs, M.: Flexible Proof-Replay with Heuristics, LSA-Report, LSA-97-03E, University of Kaiserslautern, 1997.
Fuchs, Matt.: Experiments in the Heuristic Use of Past Proof Experience, Proc. CADE 13, New Brunswick, NJ, USA, 1996.
Goller, C.; Küchler, A.: Learning Task-Dependent Distributed Representations by Back-propagation Through Structure, Proc. ICNN-96, 1996.
Knuth, D.E.; Bendix, P.B.: Simple Word Problems in Universal Algebra, Computational Algebra, J. Leech, Pergamon Press, 1970, pp. 263–297.
Kolbe, T.; Walther, C.: Reusing proofs, Proc. 11th ECAI '94, Amsterdam, HOL, 1994, pp. 80–84.
McCune, W.W.: OTTER 3.0 reference manual and guide, Techn. report ANL-946, Argonne Natl. Laboratory, 1994.
Owen, S.: Analogy for automated reasoning, Academic Press, 1990.
Suttner, C.; Ertel, W.: Automatic acquisition of search-guiding heuristics, Proc. CADE 10, Kaiserslautern, FRG, 1990, LNAI 449, pp. 470–484.
Sutcliffe, G.; Suttner, C.B.; Yemenis, T.: The TPTP Problem Library, Proc. CADE 12, Nancy, Springer LNAI 814, pp. 252–266, 1994
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fuchs, M. (1997). Flexible proof-replay with heuristics. In: Coasta, E., Cardoso, A. (eds) Progress in Artificial Intelligence. EPIA 1997. Lecture Notes in Computer Science, vol 1323. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023906
Download citation
DOI: https://doi.org/10.1007/BFb0023906
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63586-4
Online ISBN: 978-3-540-69605-6
eBook Packages: Springer Book Archive