Flexible Re-enactment of Proofs

Matthias Fuchs
Center for Learning Systems and Applications (LSA)
Fachbereich Informatik
Universitaet Kaiserslautern
Postfach 3049
67653 Kaiserslautern
Germany
E-mail: fuchs@informatik.uni-kl.de

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.

Keywords
theorem proving, machine learning, learning heuristics

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1997/
file: Fuchs.SR-97-01.ps.gz