We present a proof-of-concept prototype of a (constructive variant of an) HOL interactive theorem prover written in a higher order logic programming (HOLP) language, namely an extension of lambda Prolog. The prototype...
详细信息
ISBN:
(纸本)9781450347778
We present a proof-of-concept prototype of a (constructive variant of an) HOL interactive theorem prover written in a higher order logic programming (HOLP) language, namely an extension of lambda Prolog. The prototype is meant to support the claim, that we reinforce, that HOLP is the class of languages that provides the right abstraction level and programming primitives to obtain concise implementations of theorem provers. We identify and advocate for a programming technique, that we call semi-shallow embedding, while at the same time identifying the reasons why pure lambda Prolog is not sufficient to support that technique, and it needs to be extended.
We consider a simple extension of logicprogramming where variables may range over goals and goals may be arguments of predicates. In this language we can write logic programs which use goals as data. We give practica...
详细信息
We consider a simple extension of logicprogramming where variables may range over goals and goals may be arguments of predicates. In this language we can write logic programs which use goals as data. We give practical evidence that, by exploiting this capability when transforming programs, we can improve program efficiency. We propose a set of program transformation rules which extend the familiar unfolding and folding rules and allow us to manipulate clauses with goals which occur as arguments of predicates. In order to prove the correctness of these transformation rules, we formally define the operational semantics of our extended logicprogramming language. This semantics is a simple variant of I-D-resolution. When suitable conditions are satisfied this semantics agrees with LD-resolution and, thus, the programs written in our extended language can be run by ordinary Prolog systems. Our transformation rules are shown to preserve the operational semantics and termination.
暂无评论