First-order theories for pure Prolog programs with negation (Q1892097): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 06:07, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | First-order theories for pure Prolog programs with negation |
scientific article |
Statements
First-order theories for pure Prolog programs with negation (English)
0 references
5 July 1995
0 references
The paper is the extended version of that one which appeared in the proceedings of the Ninth Symposium on Logic in Computer Science (1994). It introduces a new form of completion, called \(\ell\)-completion, which provides a sound and complete axiomatization of the Prolog depth-first strategy under some natural conditions. A method based on \(\ell\)- completion is then investigated to prove termination and equivalence of (pure) Prolog programs with negation. The basic idea is to use three operators \(S\), \(F\) and \(T\) to construct first order formulas \(SG\), \(FG\) and \(TG\) expressing success, failure and (universal) termination of the goal \(G\), respectively. Given a program \(P\), the \(\ell\)-completion is obtained as the first order theory axiomatized by some axioms for the previous operators together with CET (Clark equality theory) and some formulas derived from \(P\). The main result then shows that a goal \(G\) succeeds (resp. fails) under Prolog resolution in the program \(P\) iff \(SG\) (resp. \(FG)\) is provable from the \(\ell\)-completion (some conditions are needed for the ``if'' part). The paper is accurate and clear, and the results obtained are certain relevant. In particular, they furnish a logical semantics for Prolog which is much more elegant than many other existing semantics based on ad-hoc, often very complicate, constructions.
0 references
prolog
0 references
completion
0 references
semantics
0 references