Using Term Space Maps to Capture Search Control Knowledge in Equational Theorem Proving

Stephan Schultz and Felix Brandt, Technische Universität München

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.