Paper Info
Title
Is there an axiomatic semantics for standard pure Prolog?
Abstract
Many studies [1, 7, 20, 21, 26, 28] have shown the soundness and completeness of SLD-resolution and of the finite failure rule for a definite program. This semantics corresponds to the operational semantics of an (ideal) Prolog system, i.e. which only generates fair SLD-trees and employs a breadth-first search rule. Unfortunately, the Prolog systems currently used may generate non-fair SLD-trees and employ a depth-first-left-right strategy which is no longer complete. For these standard Prolog implementations, the operational semantics of a program depends not only on its logic content but also on the way it is written. In this work, we introduce two systems of axioms associated to a definite program P : • the finite standard translation Ax fst which provides a logic characterization of the finite operational semantics of a definite program P computed by a Standard Prolog System and does not depend on the ordering given to the clauses in the program P . • the finite invariant translation Ax f which gives a logic characterization of the success and the failures of P , all SLD-trees of which are finite. This translation does not depend on the ordering given to the clauses in the program and to the atoms in each clause.
Year
DOI
Venue
1991
10.1016/0304-3975(91)90229-U
Theor. Comput. Sci.
Keywords
DocType
Volume
axiomatic semantics,standard pure Prolog
Journal
82
Issue
ISSN
Citations 
2
Theoretical Computer Science
0
PageRank 
References 
Authors
0.34
18
2
Name
Order
Citations
PageRank
François Denis100.34
Jean-Paul Delahaye232554.60