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].

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.