Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers

5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016)
Coimbra, Portugal


One of the reasons that forward search methods, like resolution, are efficient in practice is their ability to utilize many optimization tech- niques. One such technique is subsumption and one way of utilizing subsumption efficiently is by indexing terms using substitution trees. In this paper we describe an attempt to extend such indexes for the use of higher-order resolution theorem provers. Our attempt tries to handle two difficulties which arise when extending the indexes to higher-order. The first difficulty is the need for higher-order anti-unification. The second difficulty is the closure of clauses under associativity and com- mutativity. We present some techniques which attempt to solve these two problems.