Learning Domain Knowledge to Improve Theorem Proving

Jörg Denzinger and Stephan Schulz

appeared in:
Proc. Conference on Automated Deduction (CADE) 1996, New Brunswick, Springer, LNAI 1104, 1996, pp. 62-76.


Abstract

We present two learning inference control heuristics for equational deduction. Based on data about facts that contributed to previous proofs, evaluation functions learn to select equations that are likely to be of use in new situations. The first evaluation function works by symbolic retrieval of generalized patterns from a knowledge base, the second function compiles the knowledge into abstract term evaluation trees. We analyze the performance of the two heuristics on a set of examples and demonstrate their usefulness. We also show that these strategies are well suited for cooperation in the framework of the knowledge based distribution method teamwork.



Generated: 29/10/99