The search result changed since you submitted your search request. Documents might be displayed in a different sort order.
  • search hit 18 of 31
Back to Result List

Learning proof heuristics by adapting parameters

  • We present a method for learning heuristics employed by an automated proverto control its inference machine. The hub of the method is the adaptation of theparameters of a heuristic. Adaptation is accomplished by a genetic algorithm.The necessary guidance during the learning process is provided by a proof prob-lem and a proof of it found in the past. The objective of learning consists infinding a parameter configuration that avoids redundant effort w.r.t. this prob-lem and the particular proof of it. A heuristic learned (adapted) this way canthen be applied profitably when searching for a proof of a similar problem. So,our method can be used to train a proof heuristic for a class of similar problems.A number of experiments (with an automated prover for purely equationallogic) show that adapted heuristics are not only able to speed up enormously thesearch for the proof learned during adaptation. They also reduce redundancies inthe search for proofs of similar theorems. This not only results in finding proofsfaster, but also enables the prover to prove theorems it could not handle before.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Matthias Fuchs
URN:urn:nbn:de:hbz:386-kluedo-3421
Series (Serial Number):SEKI Report (95,2)
Document Type:Preprint
Language of publication:English
Year of Completion:1995
Year of first Publication:1995
Publishing Institution:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011