A simple mathematical definition of the 4-port model for pure Prolog is given. The model combines the intuition of ports with a compact representation of execution state. Forward and backward derivation steps are possible. The model satisfies a modularity claim, making it suitable for formal reasoning.
In contrast to the few specifications of the Byrd box, there are many more general models of pure (or even full) Prolog execution. Due to space limitations we mention here only some models, directly relevant to , and for a more comprehensive discussion see @cite_1 . Comparable to our work are the stack-based approaches. St "ark gives in @cite_3 , as a side issue, a simple operational semantics of pure logic programming. A state of execution is a stack of frame stacks, where each frame consists of a goal (ancestor) and an environment. In comparison, our state of execution consists of exactly one environment and one ancestor stack . The seminal paper of Jones and Mycroft @cite_10 was the first to present a stack-based model of execution, applicable to pure Prolog with cut added. It uses a sequence of frames. In these stack-based approaches (including our previous attempt @cite_1 ), there is no , it is not possible to abstract the execution of a subgoal.
@cite_10 @cite_1 @cite_3
158887749 2058402932 2013417779
Abstract The coincidence between the model-theoretic and the procedural semantics of SLD-resolution does not carry over to a Prolog system that also implements non-logical features like cut and whose depth-first search strategy is incomplete. The purpose of this paper is to present the key concepts of a new, simple operational semantics of Standard Prolog in the form of rewriting rules. We use a novel linear representation of the Prolog tree traversal. A derivation is represented at the level of unification and backtracking. The rewriting system presented here can easily be implemented in a rewriting logic language, giving an executable specification of Prolog. This article contains the theoretical foundations of LPTP, a logic program theorem prover that has been implemented in Prolog by the author. LPTP is an interactive theorem prover in which one can prove correctness properties of pure Prolog programs that contain negation and built-in predicates like is2 and calln + 1. The largest example program that has been verified using LPTP is 635 lines long including its specification. The full formal correctness proof is 13 128 lines long (133 pages). The formal theory underlying LPTP is the inductive extension of pure Prolog programs. This is a first-order theory that contains induction principles corresponding to the definition of the predicates in the program plus appropriate axioms for built-in predicates. The inductive extension allows to express modes and types of predicates. These can then be used to prove termination and correctness properties of programs. The main result of this article is that the inductive extension is an adequate axiomatization of the operational semantics of pure Prolog with built-in predicates.