Tech Reports

ULCS-03-017

LambdaLeanTap: Lean Deduction in Lambda Prolog

Alexei Lisitsa


Abstract

In this note, we describe lambdaleanTAP, lean tableaux prover for firstorder logic, implemented in the higher-order logic programming language lambdaProlog. It is derivative of well-known leanTAP prover [5, 6], but makes use of the higherorder unification and lambda-terms as data structures in lambdaProlog. This allows us to re-implement leanTAP in more direct and declarative way, without using the non-logical copy term predicate and with lambda-terms representing the quantifier's bindings. Overall the efficiency of such lambdaleanTAP proves to be comparable with the original leanTAP. Finally, we show the experimental results for a subset of Pelletier's problems [17].

[Full Paper]