Abstract
We present a method for making use of past proof experience called flexible re-enactment (FR). FR is actually a search-guiding heuristic that uses past proof experience to create a search bias. Given a proof P of a problem solved previously that is assumed to be similar to the current problem A, FR searches for P and in the “neighborhood” of P in order to find a proof of A.
This heuristic use of past experience has certain advantages that make FR quite profitable and give it a wide range of applicability. Experimental studies substantiate and illustrate this claim.
This work was supported by the Deutsche Forschungsgemeinschaft (DFG).
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L.; Dershowitz, N.; Plaisted, D.:Completion without Failure, Coll. on the Resolution of Equations in Algebraic Structures, Austin, TX, USA (1987), Academic Press, 1989.
Brock, B.; Cooper, 5.; Pierce, W.:Analogical Reasoning and Proof Discovery, Proc. CADE-9, Argonne, IL, USA, 1988, Springer LNCS 310, pp. 454–468.
Bundy, A.:The Use of Explicit Plans to Guide Inductive Proofs, Proc. CADE-9, Argonne, IL, USA, 1988, Springer LNCS 310, pp. 111–120.
Chang, C.L.; Lee, R.C.:Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
Denzinger, J.; Fuchs, M.; Fuchs, Marc:High Performance ATP Systems by Combining Several AI Methods, SEKI Report SR-96-09, University of Kaiserslautern, 1996, http://www.uni-kl.de/AG-AvenhausMadlener/fuchs.html.
Denzinger, J.; Schulz, S.:Learning Domain Knowledge to Improve Theorem Proving, Proc. LADE-13, New Brunswick, NJ, USA, 1996, Springer LNAI 1104, pp. 62–76.
Fuchs, D.; Fuchs, M.:CODE: A Powerful Prover for Problems of Condensed Detachment, Proc. LADE-14, Townsville, AUS, 1997, Springer LNAI, to appear.
Fuchs, M.:Learning Proof Heuristics by Adapting Parameters, Proc. 12th ICML, Tahoe City, CA, USA, 1995, Morgan Kaufmann, pp. 235–243.
Fuchs, M.:Experiments in the Heuristic Use of Past Proof Experience, SEKI Report SR-95-10, University of Kaiserslautern, 1996, obtainable via WWW at http://www.uni-kl.de/AG-AvenhausMadlener/fuchs.html.
Fuchs, M.:Powerful Search Heuristics Based on Weighted Symbols, Level, and Features, Proc. FLAIRS-96, Key West, FL, USA, 1996, pp. 449–453.
Fuchs, M.:Experiments in the Heuristic Use of Past Proof Experience, Proc. CADS-13, New Brunswick, NJ, USA, 1996, Springer LNAI 1104, pp. 523–537.
Fuchs, M.:Towards Full Automation of Deduction: A Case Study, SEKI Report SR-96-07, University of Kaiserslautern, 1996, obtainable via WWW at http://www.uni-kl.de/AG-AvenhausMadlener/fuchs.html.
Fuchs, M.:Flexible Re-enactment of Proofs, SEKI Report SR-97-O1, Univ. of Kaiserslautern,1997,http://www.uni-kl.de/AG-AvenhausMadlener/fuchs.html.
Kolbe, T.; Walther, C.:Reusing Proofs, Proc. 11th ECAI '94, Amsterdam, HOL, 1994, pp. 80–84.
Lukasiewicz, J.:Selected Works, L. Borkowski (ed.), North-Holland, 1970.
McCune, W.; Wos, L.:Experiments in Automated Deduction with Condensed Detachment, Proc. LADE-11, Saratoga Springs, NY, USA, 1992, Springer LNAI 607, pp. 209–223.
McCune, W.:OTTER 3.0 reference manual and guide, Techn. report ANL-946, Argonne Natl. Laboratory, 1994.
Melis, E.:A Model of Analogy-driven Proof-plan Construction, Proc. 14th IJCAI, Montreal, CAN, AAAl Press, 1995, pp. 182–189.
Peterson, G.J.: An Automatic Theorem Prover for Substitution and Detachment Systems, Notre Dame J. of Formal Logic, Vol. 19, No. 1, Jan. 1976, pp. 119–122.
Slagle, J.R.; Farrell, C.D.:Experiments in Automatic Learning of a Multipurpose Heuristic Program, Comm. of the ACM, Vol. 14, No. 2, 1971, pp. 91–99.
Slaney, J.:SCOTT: A Model-guided Theorem Prover, Proc. IJCAI'93, Chambery, FRA, 1993, AAAI Press, pp. 109–114.
Sutcliffe, G.; Suttner, C.; Yemenis, T.:The TPTP Problem Library, Proc. LADE-12, Nancy, FRA, 1994, Springer LNAI 814, pp. 252–266.
Suttner, C.; Ertel, W.:Automatic Acquisition of Search-guiding Heuristics, Proc. CADE-10, Kaiserslautern, FRG, 1990, Springer LNAI 449, pp. 470–484.
Tarski, A.:Logic, Semantics, Metamathematics, Oxford University Press, 1956.
Veroff, R.:, Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies, JAR 16:223–239, 1996.
Wos, L.: Meeting the Challenge of Fifty Years of Logic, JAR 6:213–232, 1990.
Wos, L.: Searching for Circles of Pure Proofs, JAR 15:279–315, 1995.
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 re-enactment of proofs. 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/BFb0023907
Download citation
DOI: https://doi.org/10.1007/BFb0023907
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