A three-valued semantics for Horn clause programs

Lee Naish

The study of semantics of logic programs has shown strong links between the model theoretic semantics (truth and falsity of atoms in the programmer's interpretation of a program), procedural semantics (for example, SLD resolution) and fixpoint semantics (which is useful for program analysis and alternative execution mechanisms). Nearly all of this work assumes that intended interpretations are two-valued: a ground atom is true (and should succeed according to the procedural semantics) or false (and should not succeed). In reality, intended interpretations are less precise. Programmers consider that some atoms "should not occur" or are "ill-typed" or "inadmissible". Programmers don't know and don't care whether such atoms succeed. In this paper we propose a three-valued semantics for (essentially) Horn clause programs which reflects this. It is simpler and more flexible than previously proposed type schemes which implicitly recognise this third truth value. It provides tools to reason about correctness of programs without the need for unnatural precision or undue restrictions on programming style. This work has been motivated by work on declarative debugging, where it has been recognised that inadmissible calls are important.

A three-valued semantics for logic programmers (a more recent paper which subsumes this one)
Tech report version: compressed dvi file (21k); compressed Postscript file (61k)
references
ACSC conference version: gzipped DVI file (21k)
ACSC conference slides: gzipped DVI file (5k)
A three-valued declarative debugging scheme

Lee