First-order theorem provers are commonly utilised as back-ends to proof assistants. In order to improve efficiency, it is desirable that such provers can carry out some higher-order reasoning. In his 1991 paper, Dougherty proposed a combinatory unification algorithm for higher-order logic. The algorithm removes the need to deal with λ-binders and α-renaming, making it attractive to implement in first-order provers. However, since publication it has garnered little interest due to a number of characteristics that make it unsuitable for a practical implementation. It fails to terminate on many trivial instances and requires polymorphism. We present a restricted version of Dougherty’s algorithm that is incomplete, terminating and does not require polymorphism. Further, we describe its implementation in the Vampire theorem prover, including a novel use of a substitution tree as a filtering index for higher-order unification. Finally, we analyse the performance of the algorithm on two benchmark sets and show that it is competitive.
CITATION STYLE
Bhayat, A., & Reger, G. (2019). Restricted combinatory unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11716 LNAI, pp. 74–93). Springer. https://doi.org/10.1007/978-3-030-29436-6_5
Mendeley helps you to discover research relevant for your work.