Skip to main content
SpringerLink
Log in

Flexible re-enactment of proofs

  • Automated Reasoning and Theorem Proving
  • Conference paper
  • First Online:
Progress in Artificial Intelligence (EPIA 1997)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1323))

Included in the following conference series:

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 to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.

    Google Scholar 

  2. Brock, B.; Cooper, 5.; Pierce, W.:Analogical Reasoning and Proof Discovery, Proc. CADE-9, Argonne, IL, USA, 1988, Springer LNCS 310, pp. 454–468.

    Google Scholar 

  3. Bundy, A.:The Use of Explicit Plans to Guide Inductive Proofs, Proc. CADE-9, Argonne, IL, USA, 1988, Springer LNCS 310, pp. 111–120.

    Google Scholar 

  4. Chang, C.L.; Lee, R.C.:Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.

    Google Scholar 

  5. 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.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. Fuchs, D.; Fuchs, M.:CODE: A Powerful Prover for Problems of Condensed Detachment, Proc. LADE-14, Townsville, AUS, 1997, Springer LNAI, to appear.

    Google Scholar 

  8. Fuchs, M.:Learning Proof Heuristics by Adapting Parameters, Proc. 12th ICML, Tahoe City, CA, USA, 1995, Morgan Kaufmann, pp. 235–243.

    Google Scholar 

  9. 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.

    Google Scholar 

  10. Fuchs, M.:Powerful Search Heuristics Based on Weighted Symbols, Level, and Features, Proc. FLAIRS-96, Key West, FL, USA, 1996, pp. 449–453.

    Google Scholar 

  11. 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.

    Google Scholar 

  12. 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.

    Google Scholar 

  13. 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.

    Google Scholar 

  14. Kolbe, T.; Walther, C.:Reusing Proofs, Proc. 11th ECAI '94, Amsterdam, HOL, 1994, pp. 80–84.

    Google Scholar 

  15. Lukasiewicz, J.:Selected Works, L. Borkowski (ed.), North-Holland, 1970.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. McCune, W.:OTTER 3.0 reference manual and guide, Techn. report ANL-946, Argonne Natl. Laboratory, 1994.

    Google Scholar 

  18. Melis, E.:A Model of Analogy-driven Proof-plan Construction, Proc. 14th IJCAI, Montreal, CAN, AAAl Press, 1995, pp. 182–189.

    Google Scholar 

  19. 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.

    Google Scholar 

  20. 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.

    Google Scholar 

  21. Slaney, J.:SCOTT: A Model-guided Theorem Prover, Proc. IJCAI'93, Chambery, FRA, 1993, AAAI Press, pp. 109–114.

    Google Scholar 

  22. Sutcliffe, G.; Suttner, C.; Yemenis, T.:The TPTP Problem Library, Proc. LADE-12, Nancy, FRA, 1994, Springer LNAI 814, pp. 252–266.

    Google Scholar 

  23. Suttner, C.; Ertel, W.:Automatic Acquisition of Search-guiding Heuristics, Proc. CADE-10, Kaiserslautern, FRG, 1990, Springer LNAI 449, pp. 470–484.

    Google Scholar 

  24. Tarski, A.:Logic, Semantics, Metamathematics, Oxford University Press, 1956.

    Google Scholar 

  25. Veroff, R.:, Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies, JAR 16:223–239, 1996.

    Google Scholar 

  26. Wos, L.: Meeting the Challenge of Fifty Years of Logic, JAR 6:213–232, 1990.

    Google Scholar 

  27. Wos, L.: Searching for Circles of Pure Proofs, JAR 15:279–315, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Center for Learning Systems and Applications (LSA), Fachbereich Informatik, Universität Kaiserslautern, Postfach 3049, 67653, Kaiserslautern, Germany

    Matthias Fuchs

Authors
  1. Matthias Fuchs
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ernesto Coasta Amilcar Cardoso

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation