OTTER-LAMBDA, A THEOREM-PROVER WITH UNTYPED LAMBDA-UNIFICATION
Michael J. Beeson · 2004
Support for lambda calculus and an algorithm for untyped lambda-unification has been implemented, starting from the source code for Otter. The result is a new theorem prover called Otter-λ. This is the first time that a resolution-based, clause-language prover (that accumulates deduced clauses and uses strategies to control the deduction and retention of clauses) has been combined with a lambda-unification algorithm to assist in the deductions. The resulting prover combines the advantages of the proof-search algorithm of Otter and the power of higher-order unification. We describe the untyped lambda unification algorithm used by Otter-λ and give several example theorems.