A theory of complete logic programs with equality

The Journal of Logic ProgrammingPublished 1 October 1984

Joxan Jaffar, Jean-Louis Lassez, Michael J. Maher

Citations96

TL;DR

A general framework for logic programming with definite clauses, equality theories, and generalized unification is presented, and the classic results for definite clause logic programs are extended in a simple and natural manner.

Abstract

Incorporating equality into the unification process has added great power to automated theorem provers. We see a similar trend in logic programming where a number of languages are proposed with specialized or extended unification algorithms. There is a need to give a logical basis to these languages. We present here a general framework for logic programming with definite clauses, equality theories, and generalized unification. The classic results for definite clause logic programs are extended in a simple and natural manner. The extension of the soundness and completeness of the negation-as-failure rule for complete logic programs is conceptually more delicate and represents the main result of this paper.

Keywords

Computer Science

Negation as Failure

2,026 Citations1978Keith Clark

It is shown that when the clause data base and the queries satisfy certain constraints, which still leaves us with a data base more general than a conventional relational data base, the query evaluation process will find every answer that is a logical consequence of the completed data base.

Journal of the ACMThe Semantics of Predicate Logic as a Programming Language

1,463 Citations1976M. H. van Emden, Robert Kowalski

In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic are investigated, and it is concluded that operational semantics is a part ofProof theory and that fixpoint semantic is a special case of model-theoretic semantics.

View PDF

Elsevier eBooksEquations and Rewrite Rules: A Survey

714 Citations1980Gérard Huet, Derek C. Oppen

The problem of "solving" equations, the problem of proving termination of sets of rewrite rules, and the decidability and complexity of word problems and of combinations of equational theories are discussed.

Journal of the ACMContributions to the Theory of Logic Programming

586 Citations1982Krzysztof R. Apt, M. H. van Emden

It is shown that nondeterministic flowchart schemata of bounded nondeterminacy are modeled by this special case of Hom clauses, and the connection between finite failure and greatest fixpoint is used to give a semantic characterization of termination, blocking, and nontermination of such flowchart Schemata.

View PDF

Information Processing LettersFixed point theorems and semantics: a folk tale

133 Citations1982J.-L. Lassez, V.L. Nguyen +1 more

This paper searches for the theorem on which the fixed point theory of recursion is based, and the difficulties encountered suggest that the authors are in the presence of a folk theorem as defined by David Hare.

Theoretical Computer ScienceClosures and fairness in the semantics of programming logic

104 Citations1984J.-L. Lassez, Michael J. Maher

The notions of closures and fair chaotic iterations are used to give a semantics to logic programs to extend the result of Apt and Van Emden (1982) and show that this procedure is sound and strongly complete with respect to both success and finite failure.

Completeness of the negation as failure rule

87 Citations1983Joxan Jaffar, Jean-Louis Lassez +1 more

It is proved here that the converse also holds, that is, the negation as failure rule is complete.

Equality For Prolog.

53 Citations1986William A. Kornfeld

The Journal of Logic ProgrammingA logical reconstruction of Prolog II

45 Citations1984M. H. van Emden, John W. Lloyd

It is shown that Prolog II can be regarded as a logic programming language, based on tree rewriting rather than logic.

SLPConceptual Basis and Evaluation Strategies for Integrating Functional and Logic Programming.

23 Citations1984P. A. Subrahmanyam, Jia-Huai You