We describe a learning inference control heuristic for an equational theorem prover. The heuristic selects a number of problems similar to a new problem from a knowledge base and compiles information about good search decisions for these selected problems into a term space map, which is used to evaluate the search alternatives at an important choice point in the theorem prover. Experiments on the TPTP problem library show the improvements possible with this new approach.
Published Date: May 1999
Registration: ISBN 978-1-57735-080-4
Copyright: Published by The AAAI Press, Menlo Park, California.