## Flexible Proof-Replay with Heuristics

• We present a general framework for developing search heuristics for au-tomated theorem provers. This framework allows for the construction ofheuristics that are on the one hand able to replay (parts of) a given prooffound in the past but are on the other hand flexible enough to deviate fromthe given proof path in order to solve similar proof problems. We substanti-ate the abstract framework by the presentation of three distinct techniquesfor learning appropriate search heuristics based on soADcalled features. Wedemonstrate the usefulness of these techniques in the area of equational de-duction. Comparisons with the renowned theorem prover Otter validatethe applicability and strength of our approach.

### Weitere Dienste

Verfasserangaben: Marc Fuchs urn:nbn:de:hbz:386-kluedo-536 LSA Report (97,3E) Preprint Englisch 1997 1997 Technische Universität Kaiserslautern 03.04.2000 Fachbereich Informatik 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581$