Term Space Mapping for DISCOUNT
Stephan Schulz
We present a learning inference control heuristic implemented for the
equational theorem prover DISCOUNT. Information about necessary and
superfluous facts generated during successful proof searches ({\em
positive\/} and {\em negative} examples) is compiled into a {\em term
space map}, a recursive structure describing aspects of the topology
of term sets. This map is then used to compute evaluations for facts
in new proof searches and thus to guide the proof search. We present
results of the learning system on a set of TPTP examples and
demonstrate its usefulness.