Abstract
First-order theorem provers are commonly utilised as backends 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 its poor characteristics. 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 a significant step forward.
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 its poor characteristics. 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 a significant step forward.
| Original language | English |
|---|---|
| Title of host publication | Automated Deduction – CADE 27 |
| ISBN (Electronic) | 978-3-030-29436-6 |
| DOIs | |
| Publication status | E-pub ahead of print - 20 Aug 2019 |
| Event | The 27th International Conference on Automated Deduction - UFRN/Hotel Praiamar, Natal, Brazil Duration: 23 Aug 2019 → 30 Aug 2019 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 11716 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | The 27th International Conference on Automated Deduction |
|---|---|
| Abbreviated title | CADE27 |
| Country/Territory | Brazil |
| City | Natal |
| Period | 23/08/19 → 30/08/19 |