# A Kripke-Kleene Semantics for Logic Programs

@article{Fitting1985AKS, title={A Kripke-Kleene Semantics for Logic Programs}, author={Melvin Fitting}, journal={J. Log. Program.}, year={1985}, volume={2}, pages={295-312} }

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. In [7] Kleene proposed a three-valued logic for use in recursive function theory. The so-called third truth value was really undefined: truth value not determined. This logic is a useful tool in logic-program specification… Expand

#### Topics from this paper

#### 615 Citations

A three-valued semantics for logic programmers

- Computer Science
- Theory and Practice of Logic Programming
- 2006

A three-valued semantics for pure Prolog programs with (ground) negation as failure which reflects this is proposed, and the semantics of Fitting is similar but only associates the third truth value with non-termination. Expand

Legality Concepts for Three-Valued Logic Programs

- Mathematics, Computer Science
- Theor. Comput. Sci.
- 1993

A three-valued Horn logic is presented, where the third value has the meaning of “illegal”, i.e. unacceptable, and it is shown that the legality check of aThree-valued logic program can be also carried out through SLD resolution. Expand

Combining Negation as Failure and Embedded Implications in Logic Programs

- Mathematics, Computer Science
- J. Log. Program.
- 1998

This paper develops a top-down query evaluation procedure, a Kripke/Kleene fixed point semantics, and a logical interpretation by means of a completion construction for a language which combines embedded hypothetical implications and negation as failure (NAF). Expand

A Kripke-Kleene Logic over General Logic Programs

- Computer Science
- KI
- 1994

This work proposes a logic for partial reasoning over all general logic programs in a certain first-order language L and introduces the notion of truth for formulas of L*. Expand

QUASI-STABLE SEMANTICS OF LOGIC PROGRAMS

- 1998

1. Introduction The semantics of logic programming and deductive databases has been extensively studied in the past two decades. Many semantic theories have been proposed (see 3] for a survey). In… Expand

Truth versus information in logic programming

- Computer Science
- Theory and Practice of Logic Programming
- 2013

It is suggested that the additional truth values of Fitting/Kunen and Naish are best viewed as duals, and Belnap's four-valued logic is used, used elsewhere by Fitting, to unify the two three-valued approaches. Expand

Hypothesis-based semantics of logic programs in multivalued logics

- Mathematics, Computer Science
- TOCL
- 2004

The problem of defining semantics for logic programs in presence of incomplete and contradictory information coming from different sources is addressed and a formal framework based on bilattices such as Belnap's four-valued logics is proposed. Expand

Well-Founded Semantics, Generalized

- Computer Science
- ISLP
- 1991

It is shown how the well-founded approach also extends naturally to the same family of bilattice-based programming languages that the earlier fixpoint approaches extended to, and provides a natural semantics for logic programming systems that have already been proposed. Expand

Negation as Inconsistency in PROLOG via Intuitionistic Logic

- Computer Science
- CSL
- 1993

A semantics for negation as inconsistency based on the intuitionistic logic is suggested and the completeness result in both propositional and predicate cases is obtained. Expand

A Rewrite Mechanism for Logic Programs with Negation

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 1998

This paper shows that an extension of linear completion for pure logic programs can be built in a natural way, with ideas from the Clark completion, and the domain of constrained rewriting, and can operationally go beyond Kunen's semantics, if desired. Expand

#### References

SHOWING 1-10 OF 17 REFERENCES

Logic Programs and Many-Valued Logic

- Computer Science
- STACS
- 1984

It is claimed that the well-known equivalence of declarative and procedural interpretations for Horn clauses (predicate logic or Prolog programs) has been unjustifiably used when discussing computation and supports the view that strong correctness should be considered, rather than weak correctness together with a separate analysis of termination. Expand

The Recursion-Theoretical Complexity of the Semantics of Predicate Logic as a Programming Language

- Computer Science
- Inf. Control.
- 1982

The purpose here is to use a connection between the semantics of predicate logic as a programming language and the well-studied theory of inductive definability to given a measure to the incompleteness of the negation as failure rule for proving Herbrand valid negations of formulas, and to show that the negators of this rule are very highly incomplete in the sense of the measure. Expand

Contributions to the Theory of Logic Programming

- Mathematics, Computer Science
- JACM
- 1982

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. Expand

Negation as Failure

- Computer Science, Mathematics
- Logic and Data Bases
- 1977

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. Expand

Notes on the mathematical aspects of Kripke's theory of truth

- Mathematics, Computer Science
- Notre Dame J. Formal Log.
- 1986

Kripke's Theory of Truth is one of the most interesting developments to come along in this area for some time but the mathematical difficulties may have prevented a wider appreciation of its philosophical virtues, so this primarily expository paper largely skip over philosophical motivation. Expand

First-Order Logic

- Mathematics
- 1968

I. Propositional Logic from the Viewpoint of Analytic Tableaux.- I. Preliminaries.- 0. Foreword on Trees.- 1. Formulas of Propositional Logic.- 2. Boolean Valuations and Truth Sets.- II. Analytic… Expand

A LATTICE-THEORETICAL FIXPOINT THEOREM AND ITS APPLICATIONS

- Mathematics
- 1955

1. A lattice-theoretical fixpoint theorem. In this section we formulate and prove an elementary fixpoint theorem which holds in arbitrary complete lattices. In the following sections we give various… Expand

The Theoretical Aspects of the Optimal Fixed Point

- Mathematics, Computer Science
- SIAM J. Comput.
- 1976

A new type of fixedpoint of recursive definitions is defined that contains the maximal amount of “interesting” information which can be extracted from the recursive definition, and it may be strictly more defined than the program’s least fixedpoint. Expand

The optimal approach to recursive programs

- Mathematics, Computer Science
- CACM
- 1977

A new approach is described which introduces an “optimal fixedpoint” which, in contrast to the least defined fixedpoint, embodies the maximal amount of valuable information embedded in the program. Expand

Outline of a Theory of Truth

- Computer Science
- 1975

The JSTOR Archive is a trusted digital repository providing for long-term preservation and access to leading academic journals and scholarly literature from around the world, supported by libraries, scholarly societies, publishers, and foundations. Expand