Equivalences of Logic Programs
Elsevier eBooksPublished 1 January 1988
Michael J. Maher
Citations107
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This paper provides a systematic comparison of the relative strengths of various formulations of equivalence for logic programs and introduces the notion of subsumption-equivalence, which is used to give syntactic characterizations of the programs P for which the function TP satisfies some continuity properties.
Abstract
For applications such as deductive databases employing the Open World Assumption, failed derivations have a lesser importance. In this case, use of the identical equivalences based upon the functional semantics [P] and the logical consequences of P allows the application of two different and powerful tools to reason about programs. In particular, these equivalences seem ideal for discussing the deductive structure of such deductive databases, independent of any particular state of the database of facts.
Keywords
Computer Science
Constraint logic programming
1,613 Citations1987Joxan Jaffar, J.-L. Lassez
A class of programming languages, the CLP languages, are defined, all of which share the same essential semantic properties, and are highly declarative and are soundly based within a unified framework of formal semantics.
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.
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.
The Journal of Logic ProgrammingA kripke-kleene semantics for logic programs*
539 Citations1985Melvin Fitting
The use of conventional classical logic is misleading for characterizing the behavior of logic programs because a logic program, when queried, will do one of three things: succeed with the query, fail with it, or not respond because it has fallen into infinite backtracking.
Artificial IntelligenceA polymorphic type system for prolog
262 Citations1984Alan Mycroft, Richard O’Keefe
A polymorphic type scheme for Prolog is described which makes static type checking possible and it is observed that the type resolution problem for a Prolog program is another Prolog (meta)program.
Journal of the ACMDerivation of Logic Programs
130 Citations1981C. J. Hogger
Treating predicate logic as both a specification language and a programming language, firstorder logical deduction is shown to be sufficient for verifying, synthesizing, and transforming programs.
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.
BIT Numerical MathematicsHorn clause computability
97 Citations1977Sten-Åke Tärnlund
It is proved that a Turing computable functionf is computable in binary Horn clauses, which are a subset of first order logic and do not need more than one function symbol.
The Journal of Logic ProgrammingA theory of complete logic programs with equality
96 Citations1984Joxan Jaffar, Jean-Louis Lassez +1 more
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.
Parallel evaluation of recursive rule queries
86 Citations1985Stavros S. Cosmadakis, Paris C. Kanellakis
The main thrust of the investigation is to draw a -line between recursive qucrics that can be evaluated by NC algorithms and recursive queries that are complete in PTIME, which is motivated by the current research on pamIle implementations of PROLOG.
Journal of the ACMOn the efficiency of subsumption algorithms
67 Citations1985Georg Gottlob, Alexander Leitsch
The costs of subsumption algorithms are analyzed by an estimation of the maximal number of unification attempts made for deciding whether a clause C subsumes a clause D, which yields a lower bound for the worst-case time complexity.
The Journal of Logic ProgrammingCanonical logic programs
32 Citations1986Joxan Jaffar, Peter J. Stuckey
The main result in this paper proves that this class of programs P is representative of all programs and that for any program P1, there exists a semantically equivalent program P2 which is canonical.
Lecture notes in computer scienceSome issues and trends in the semantics of logic programming
28 Citations1986Joxan Jaffar, J.-L. Lassez +1 more
This work has seen that the gap between theory and programming practice can be reduced by introducing user-oriented domains into the formalism, and can be achieved without losing the important properties of definite clauses.