A three-valued semantics for Horn clause programs

Lee Naish

(lee@cs.mu.OZ.AU, http://www.cs.mu.oz.au/˜ lee)

Technical Report 98/4

Department of Computer Science University of Melbourne Parkville, Victoria 3052 Australia

Abstract

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.

1 Introduction

When programming, we often give too little attention to the meaning of our code. For these sins of sloth and pride (“I can’t be bothered re-checking everything — I’m sure I got it right”) we are forced to do penance, in the form of debugging. During the repetitive tedium we contemplate the relationships between our code, its behaviour and our desires: the domain of programming language semantics. Thus (in retrospect) it is natural for work on debugging to lead to work on semantics. All to often, work on semantics seems unrelated to any stage of the software life cycle. Here our aim is to provide theoretical support which can allow programmers to reason about the correctness of their code more easily.

The starting point for this work was declarative debugging of logic programs. The conventional view of the semantics of logic programs [Llo84] and declarative debugging [Sha83] [Llo87] is as follows. Every ground atom is either true or false in the intended interpretation of the program. True atoms should succeed and false atoms should fail. Declarative debuggers compare the behaviour of programs with the intended interpretation (obtained by asking questions of the programmer) in order to isolate the bug. It has been noted by various researchers that this strict division into true and false does not correspond to the intentions of typical programmers. There are some atoms encountered during debugging which simply should not occur (for example, “ill-typed” atoms). Whether they succeed or fail is not the issue. A third truth value, inadmissible, has been introduced into declarative debugging for such atoms [Per86] [PC88] [Nai97b]. This is a recognition that, in practice, intended interpretations are three-valued rather than two-valued. Similarly, most work on formal specifications allows for the behaviour of a module to be unspecified if preconditions are violated. The aim of this paper is to reconstruct the semantics of logic programs with this in mind.

The paper is structured as follows. The next sections review previous approaches to the semantics of logic programming and declarative debugging in more depth. We discuss type schemes for logic programming due to the close relationship between types an admissibility. We then present our three-valued semantics, covering operational semantics, fixpoint semantics, model theoretic semantics and the relationships between them. We make some comments about how negation could be handled before concluding.

2 Previous approaches to semantics

2.1 Traditional untyped semantics

The traditional approach to the semantics of logic programs, described in [Llo84], includes model theory, fixpoint theory and an operational semantics. Here we just discuss the theory as it applies to successful computations using Horn Clauses. That is, we do not deal with failure or negation, which lead to significant additional complication and various conflicting proposed semantics.

The model theory is two-valued — each (ground) atom in the Herbrand base is associated with the truth value true or false. Typically the theory represents an interpretation as a single set of atoms — the atoms which are true. The classical truth tables for conjunction and implication are used. The intended interpretation of a (correct) program is assumed to be a model (every clause instance is true according to the interpretation and truth tables) and this implies soundness of computations (see below). This is the great advantage of the model-theoretic semantics: a program can be viewed completely declaratively and the correctness of each clause can be verified statically and in isolation. It can also be used as the basis for declarative debugging. The intersection of two models is a model, hence a least model exists which is the intersection of all models. This is the set of logical consequences of the program. It is also the least Herbrand model.

The fixpoint semantics of a program P are based on the immediate consequence operator T_{P}, which maps a set of ground atoms M to the set of ground atoms which can be proven from M by applying a single program clause:

T_{P} (M) = {H|H ← B_{1}, B_{2}, … B_{N} is a ground clause instance and {B_{1}, B_{2}, … B_{N}} ⊆ M}

T_{P} is monotonic, and applying T_{P} n times starting with the empty set (T_{P} ↑ n) is of interest. It gives a “bottom up” semantics where initially we assume nothing and iteratively prove that a growing set of atoms are true. The least fixpoint of T_{P} is T_{P} ↑ ω (= lub(T_{P} ↑ n), n = 1, 2, …). M is a model of P if and only if T_{P} (M) ⊆ M and the least fixpoint is the least model. The fixpoint semantics are particularly useful for program analysis and have also been used as the basis for bottom up operational semantics, especially for logic databases.

The operational model is SLD resolution. This gives a top down semantics where atoms are proved by recursively proving the bodies of matching clauses. The set of (ground) atoms which have successful SLD derivations is called the success set and is independent of the computation rule (the order in which atoms are selected). The success set is the same as the least model and the least fixpoint. Thus (assuming that the intended interpretation is a model) the computed answers of a program are true in the intended interpretation.

The major flaw in this otherwise beautiful picture is that, in practice, the intended interpretation is generally not a model. Consider the example from [Llo84] in which intended interpretations are discussed:

perm([], []).
perm(X.Y, U.V) :- delete(U, X.Y, Z), perm(Z, V).
delete(X, X.Y, Y).
delete(X, Y.Z, Y.W) :- delete(X, Z, W).

It is stated “The intended meaning of the predicate delete is that delete(X,Y,Z) should hold if Z is the list obtained by deleting the element X from the list Y. The above definition for delete contains obviously correct statements about the delete predicate.” The second sentence is not true: the base case for delete does not constrain Y to be a list and is false in the intended interpretation. Calls to delete which contain non-lists and are false in the intended interpretation can succeed.

When code is written there are nearly always implicit assumptions about the context in which it is called. For delete it is assumed that the context of the call ensures that the arguments will be lists and indeed, when delete is called from perm this is the case. However, with a buggy version of perm (or if delete was called directly in the wrong context) the dubious meaning of delete can become a problem. If delete succeeds with non-lists then the conventional semantics leads us to conclude that delete contains a bug whereas the bug is really in the calling code.

Often the assumptions about the calling context concern what are normally called types (for example, lists), though they can also be more complex. For example, the merge procedure, which merges two sorted lists, is normally coded using the assumption that the first two arguments are sorted lists. Type definition languages are normally designed with static checking in mind and since sortedness is very difficult to check statically it cannot be expressed in most type languages.

2.2 Traditional typed semantics

Some logic languages, such as Gödel [HL94] and Mercury [SHC95] have used type systems similar to those used in functional programming languages, after [MO84]. Types are declared (or possibly inferred) and the type checker rejects programs which may result in atoms with incorrect argument types. The intended interpretation is typed and atoms with incorrect argument types have no meaning: they are considered ill-formed rather than true or false. This avoids the semantics problems with predicates such as delete. However, the problems remain with predicates such as merge where the assumptions made cannot be expressed in the type language.

The type language is restricted so that type checking can be performed statically, rejecting all programs which could result in ill-typed atoms. The extra discipline forced on programmers and the use of a type checker result in many bugs being detected statically. However, strong type checking also rejects many programs which would otherwise work correctly. Programmers who are used to the flexibility of untyped languages such as Prolog often object to such restrictions on their programming style.

2.3 More flexible typed semantics

The type scheme of [Nai92] was designed to solve the semantic difficulties discussed so far, while restricting correct programs as little as possible. Types in this scheme can be defined by arbitrary Horn clause programs. This allows the assumptions of predicates such as merge to be expressed by types. The intended interpretation is two valued and the true atoms should be the intersection of the success set and the set of well typed atoms. The false atoms are ill-typed or should not succeed. Our three-valued approach can be seen as a reconstruction of this type scheme using a three-valued logic (with some technical improvements): the ill-typed atoms become inadmissible rather than false.

The declarative semantics of a program P containing type declarations is given by the traditional untyped semantics of a related program S. S has the clauses of P with additional type checks added plus the definitions of the types. For example, the delete procedure would have additional calls in the body of each clause to ensure that the arguments of the clause head are lists. The intended interpretation is assumed to be a model of this program.

The procedural semantics uses the original program P, without additional type checks. To ensure soundness a restriction on programs is introduced. As well as the intended interpretation being a model of S, it is assumed that P is type correct. A definite program is defined to be type correct if for all ground clause instances H ← B such that H is well typed and B succeeds, B is well typed. Type correctness ensures that well-typedness is inherited from clause heads to clause bodies in successful derivations. Thus a well typed atom which succeeds must have a well typed refutation using P and hence would also succeed using S. Note that type correctness is not a necessary condition for soundness. A type incorrect clause whose head is true just results in a dubious “proof” of a true atom.

3 Three-valued declarative debugging

A general scheme for declarative debugging using three truth values is described in [Nai97b]; it is based on a more traditional two-valued scheme [Nai97a]. Computations are represented as trees and debuggers search the tree for a buggy node. For diagnosing wrong answers in Prolog, the tree is a proof tree (see [Llo84]): each node contains an atom which was proved in the computation and the children of the node contain the atoms in the body of the clause instance which was used at the top level of the proof. Each node has a truth value associated with it: correct, if the atom is valid (all instances are true) in the intended interpretation, erroneous, if the atom is not valid, or inadmissible, the third truth value. If a node is erroneous but all its children are correct, it corresponds to an incorrect clause instance: the body is valid but the head is not. This class of bugs was identified in the first work on declarative debugging [Sha83].

Another class of bugs, related to inadmissibility, was identified in [Per86] and formalised more in [Nai97b]: nodes which are erroneous with no erroneous children but at least one inadmissible child. In a top-down execution this corresponds to a clause instance which causes a transition from admissible atoms to inadmissible atoms. It allows an inadmissible atom which happens to succeed to be used in the proof of at atom which should not succeed.

Several different instances of the three-valued declarative debugging scheme were identified, using different definitions of inadmissibility. Although our previous work on types and debugging provides the intuition for this paper, we do not rely on any particular definition of inadmissibility here. We simply assume that the programmer has some notion of (in)admissibility and that admissibility is closed under instantiation. If inadmissibility is identified with ill-typedness (as suggested in [Per86] and [Nai92]) then the second class of bugs correspond to clauses which are not type correct. However, this definition of inadmissibility does not lead to ideal behaviour of debuggers [Nai97b] and does not quite capture the intentions of programmers.

As well as considering types, programmers consider modes. A successful call to merge in which the first argument is not a sorted list is very different from a successful call where the just last argument is not a sorted list. In the first case we would consider that the input is wrong and the bug is in the caller and in the second case we would consider that the output is wrong and the bug is in merge. A more natural definition of inadmissibility for ground atoms is that the “input” arguments of the atom are ill-typed (or violate some assumption). In [Nai97b] this definition of inadmissibility is related to a declarative view of modes [Nai96], which gives a more technical definition that captures the intuitive idea of input arguments being ill-typed.

4 Three-valued semantics

Our aim is to provide a semantics for Horn clause programs. However, we use a slight variant, disjunctive clauses, so that conjunction and disjunction can be treated more uniformly in the logic. In a disjunctive clause program each predicate is defined by a single clause H ← (B_{1} ∨ B_{2} ∨ … ∨ B_{n}), where each B_{i} is a conjunction of atoms. Disjunctive clause programs can be mapped to Horn clauses programs trivially: each disjunct leads to a clause. Horn clauses programs can easily be mapped to disjunctive clause programs by renaming variables, converting some head unification into calls to an equality predicate and combining all clauses for a predicate into a single disjunctive clause. This is similar to the completion of a program [Cla78], but the equality predicate can be defined using disjunctive clauses in the normal way, X=X, rather than being treated specially.

An intended interpretation associates each atom with one of three truth values: true, false or inadmissible. We sometimes abbreviate these to T, F and I. We also use these letters to refer to sets of atoms assigned that truth value. When describing interpretations we use the notation < I, T > for the interpretation which maps the (ground) atoms in I to inadmissible, the atoms in T to true and other atoms to false. Inadmissible atoms may succeed or fail according to the procedural semantics but this distinction is not made in the declarative semantics. Our semantics is thus less precise than the traditional semantics, to reflect the lack of precision of programmers. If we consider calls to merge where the first two arguments are sorted lists then programmers typically know which ones should succeed. For other (inadmissible) calls to merge, programmers typically don’t know and don’t care precisely which calls succeed. Our semantics aims at providing tools to reason about program correctness without the need for additional precision and without unnecessary restrictions on programming style. We define operational, fixpoint and model theoretic semantics then discuss the relationships between them.

4.1 Operational semantics

The operational semantics are essentially the same as SLD resolution or pure Prolog execution. Instead of a nondeterministic clause selection followed by (possibly failed) unification and construction of the resolvent we have (possibly failed) unification followed by nondeterministic disjunct selection and construction of the resolvent. A refutation of an admissible atom A which contains inadmissible atoms is suspect. Our definition of a model (see later) includes a condition similar to type correctness, ensuring soundness.

4.2 Fixpoint semantics

We define C_{P} (an analogue of T_{P}) which returns a set of atoms given two sets of atoms as arguments. The second argument is analogous to the argument of T_{P} and the first is the inadmissible atoms. To mirror the programmers view, inadmissible atoms can succeed. C_{P} returns the set of admissible atoms which can be deduced in one step from the atoms in its arguments:

C_{P} (I, T) = {H|H ← D_{1} ∨ D_{2} ∨ … D_{N} is a clause instance; all atoms in D_{i} are in I ∪ T } \ I

C′_{P} takes an interpretation and maps it to an interpretation, preserving the set of inadmissible atoms:

C′_{P} (< I, T >) =< I, C_{P} (I, T) >

C_{P} (I) ↑ n and C_{P} (I) ↑ ω are defined in a similar way to T_{P} ↑ n and T_{P} ↑ ω:

C_{P} (I) ↑ 0 = < I, ϕ >
C_{P} (I) ↑ (n + 1) = C′_{P} (C_{P} (I) ↑ n)

C_{P} (I) ↑ ω =< I, lub(T_{n}) >, n = 1, 2, … where T_{n} is s.t. C_{P} (I) ↑ n = < I, T_{n} >

These operators have essentially the same monotonicity and fixpoint characteristics as T_{P}. C′_{P} (< ϕ, M >) and C_{P} (ϕ) ↑ n are equivalent to T_{P} (M) and T_{P} ↑ n, respectively, except for the additional (empty) set in the argument and result. If we define P ⊕ I to be the program P with additional facts (or disjunctions) so that all atoms in I succeed in one step then C′_{P} (< I, M >) and C_{P} (I) ↑ n are the same as T_{P ⊕I}(M) and T_{P ⊕I} ↑ n, respectively, except that the atoms in I are separated^{1}.

4.3 Model-theoretic semantics

We first define interpretations and models then discuss the motivation for these definitions and the properties of models.

Definition An interpretation is a mapping from ground atoms to the truth values true, false and inadmissible.

Conjunction and disjunction are defined as below:

\begin{matrix}X ∧ Y & T & F & I \\ T & T & F & I \\ F & F & F & F \\ I & I & F & I \end{matrix}  \begin{matrix}X ∨ Y & T & F & I \\ T & T & T & T \\ F & T & F & I \\ I & T & I & I \end{matrix}

Definition An interpretation is a model of a program P if no instance of a clause in P is mapped (by the interpretation and definitions of conjunction and disjunction) to F ← T or F ← I.

Note that the traditional two-valued model theory is a special case of these definitions where the set of inadmissible atoms is empty. We have attempted to make the definition of a model as weak as possible, to avoid restricting programs unnecessarily: it just avoids the two classes of bugs discussed earlier. The definitions of conjunction and disjunction follow the same principle.

For conjunction, the key question is whether I ∧ F should equal I or F. A choice of I would be similar to strict type schemes in which a conjunction containing an ill-typed atom is ill-typed, whether it succeeds or fails. Programs are restricted so that all derivations are well typed, not just successful ones (distinguishing between these two cases cannot be done statically). The choice of F is similar to less restrictive type schemes which only restrict successful derivations; this is discussed further in [Nai92]. It allows runtime checking of types (or other assertions) to be supported. The body of a clause instance can have checks which fail (have truth value F) as well as inadmissible calls, that is, the clause is of the form F ← F ∧ I. This would not be acceptable with the stricter definition of conjunction.

For disjunction, the key question is whether I ∨ T should equal I or T. In strict type schemes a disjunction containing an ill-typed atom is ill-typed even if a well-typed disjunct succeeds. Even in the less strict scheme of [Nai92] disjunctions must be implemented as separate clauses and each clause must be type correct. This is the reason we introduced disjunctive clauses: by choosing T we can have a less restrictive condition.

In some cases the type correctness condition of [Nai92] is less restrictive than our condition for an interpretation to be a model. Comparison of the two is simplified if we identify admissibility with well-typedness. Our definition of a model is purely declarative, relying just on the distinction between the three truth values. Type correctness is defined in terms of a mixture of procedural and declarative notions, relying on distinctions between successful and unsuccessful atoms and between admissible and inadmissible atoms. Clauses of the form F ← I are allowed if body fails (without procedural knowledge we must assume the worst: all inadmissible atoms succeed). However, type correctness does not take full advantage of declarative information. No distinction is made between T and F, so clauses of the form T ← I (and T ← I ∨ T) are rejected unnecessarily.

1Technically, P ⊕ I may be an infinite program. This causes no problems for T_{P} or success in general, though more care must be taken when dealing with finite failure and negation

The structure of the set of all models is more complex than the two-valued case. There are two model intersection properties of interest:

Proposition 4.1 If < I_{1}, T > and < I_{2}, T > are models then < I_{1} ∩ I_{2}, T > is a model.

Proof All three interpretations have the same set of atoms with truth value T. If the intersection has an atom which is F then it must be F in one of the other interpretations. If the intersection has a formula which is I then it must be I in both other interpretations (by inspection of the truth tables and induction on the number of connectives). Hence, if there is a clause instance of the form F ← I or F ← T in the intersection there is such an instance in one of the other interpretations. ⋄

Proposition 4.2 If < I, T_{1} > and < I, T_{2} > are models then < I, T_{1} ∩ T_{2} > is a model.

Proof If there is a clause instance whose body is I in the intersection then it must be either I or T in the other two models. The head therefore cannot be F in either of these models and hence cannot be F in the intersection. If there is a clause instance whose head is F in the intersection then it must be F in one of the other two models. The body therefore be F in this model and hence must be F in the intersection. ⋄

From these two propositions it follows that a least model of the form < ϕ, T > exists and a least model of the form < I, ϕ > exists. These two models have the same set of false atoms (just the role of true and inadmissible are swapped — the truth tables are equivalent if either true or inadmissible are ignored). These models are equivalent to the least two-valued model of the program.

Proposition 4.3 If < I, T > is a model then < I ∪ T, ϕ > is a model.

Proof Any formula which is inadmissible or true according to < I ∪ T, ϕ > must be inadmissible or true according to < I, T > (by inspection of the truth tables) so there is no clause instance of the form F ← I or F ← T according to < I ∪ T, ϕ >. ⋄

Proposition 4.4 If < I, T > is a model then I ∪ T contains the least two-valued model.

Proof < I ∪ T, ϕ > must be a model and contain the least model with no true atoms. ⋄

Thus we have a set of (at least two) minimal models, all with the same set of false atoms.

4.4 Relationships between semantics

The relationship between three-valued models and C_{P} is identical to the relationship between two-valued models and T_{P}:

Proposition 4.5 < I, T > is a model iff C_{P} (I, T) ⊆ T.

Proof C_{P} (I, T) ⊆ T iff atoms which are false in < I, T > are also false in < I, C_{P} (I, T) > iff there is no clause instance of the form F ← I or F ← T (by inspection of the truth tables). ⋄

The relationship between least fixpoints, minimal models and success set is more complex than the two-valued case. We have a choice for the set of inadmissible atoms in C_{P} and there are multiple minimal models.

Proposition 4.6 lfp(C_{P} (ϕ)) = C_{P} (ϕ) ↑ ω = the set of true and inadmissible atoms in the minimal models = SS.

Proof C_{P} (ϕ) is equivalent to T_{P} and so the results follow from the two valued case and the results concerning minimal models. ⋄

The main theorem we have concerns soundness for admissible atoms. A successful atom may not be true, since inadmissible atoms can succeed. However, an admissible atom which succeeds must be true if the intended interpretation is a model.

Theorem 4.1 (Soundness for admissible atoms) If < I, T > is a model, A is admissible and A ∈ SS then A is true.

Proof I ∪ T ⊇ SS by the propositions above. The result follows. ⋄

A form of completeness is inherited from the two-valued case:

Theorem 4.2 If A is true or inadmissible in every model then A ∈ SS.

This result is not really useful in practice for two reasons. First, although it is straightforward for a programmer to determine if her intended interpretation is a model, it is very difficult to determine if it is a minimal model. The condition in the theorem is not something a typical programmer would want to think about. Second, even if A is in the success set, the unfair search strategy of Prolog may not find a proof. Even a fair search strategy may exhaust some resource limit before finding a proof.

5 Negation

When negation is introduced, many of the convenient properties of the semantics of logic programs break down. For example, the model intersection property no longer holds, the immediate consequence operator is no longer monotonic and in the procedural semantics negation is generally associated with finite failure which is dependent on the computation rule. There is (very) extensive work in this area, including some three-valued approaches [FBJ88][Kun87]. The work tends to be directed at solving mathematical and computational problems in order to make the declarative and procedural semantics as close as possible, and there is a general desire to be able to assign a meaning to all possible programs.

In our view, both these goals are questionable. The declarative semantics should support a notion of inadmissibility which is not tied down to any particular program behaviour, thus leading to an inevitable gap between declarative and procedural readings. The key question for programmers is whether a program is correct according to their intended interpretation. If the answer is no, one possible solution is to change the intended interpretation (having a semantics for every program is useful here). However, the more common solution is to change the program!

The first and simplest approach to negation was to use the negation as failure rule for the operational semantics and Clark’s completion for the declarative semantics [Cla78]. Here we sketch how this approach could be adapted to our three-valued scheme. For disjunctive clauses the completion can be formed by converting head unification into calls to an equality predicate in each disjunct in the clause, adding equality axioms and treating each clause as an if and only if definition. Negation must be defined for the third truth value: ¬I = I. Clauses of the form T ↔ F are a source of incompleteness (a class of bugs called uncovered atoms [Sha83]) which can translate to unsoundness when negation as failure is used. Models of the completion would therefore not include such clauses. Clauses of the form I ↔ F seem not to cause problems for Prolog’s top-down execution mechanism, though they might cause unsoundness with other procedural semantics (such as bottomup execution). Some problems with Clark’s approach are solved by using three valued interpretations. For example, although the completion may have no two-valued models, a three-valued model always exists (for example, everything can be inadmissible). We plan to investigate this properties of this approach further.

6 Conclusion

In this work we have been trying to find a better answer to the following question. What is the weakest condition a programmer should enforce which ensures correct behaviour of their programs? In the current context we identify correct behaviour with soundness, though in general, forms of completeness, termination and even efficiency are important. The traditional answer is that the programmer should have a two-valued interpretation which a model of the program. Our answer is that the programmer should have a three-valued interpretation which a model of the program. This is a weaker condition, the traditional approach being a particular instance.

Can we do better still? The interpretation being a model is not a necessary condition for soundness, so technically weaker conditions do exist. One possibility is for the programmer to distinguish between successful and unsuccessful inadmissible atoms, so we can allow clauses of the form F ← I where the body doesn’t succeed. The other possibility is to allow clauses of the form F ← T, where the body doesn’t succeed. This essentially requires the programmer to recognise atoms which are true in some models but not all models. We have argued that programmers should not have to make these distinctions and in practice often do not make them (hence the intentions of programmers do not correspond to two-valued models, violating the most fundamental assumption of the traditional approach).

If the programmer does go to the trouble of making these distinctions then their interpretation can be changed to reflect this. In the case of inadmissible atoms which are know to not succeed, their truth value can be changed to false (moving closer to the traditional two-valued semantics). For atoms which are known to be true in only some models, their truth value could be changed to inadmissible (this is an attractive option if we consider models of the completion since such atoms cause nontermination with the Prolog evaluation strategy). Thus the programmer can use additional knowledge of the code to arrive at (less natural) interpretations, but this additional knowledge is not necessary.

From a more technical perspective, the model theory seems quite elegant. The fixpoint theory is more complex than the two-valued case but retains the important relationship with the model theory. Our semantics is very programmer-oriented, giving no immediate help to those interested in automatic program analysis. However, if programmers communicate additional information about their intended interpretation, for example, declare (an approximation to) the set of inadmissible atoms, then this could be used for program analysis. Potentially we could build more flexible transformation and optimisation tools which need not preserve the behaviour of inadmissible atoms. It may also allow more flexible verification of code with respect to specifications which include preconditions.

References

[Cla78] Keith L. Clark. Negation as failure. In Herve Gallaire and Jack Minker, editors, Logic and data bases, pages 293–322. Plenum Press, 1978.

[FBJ88] Melvin Fitting and Marion Ben-Jacob. Stratified and three-valued logic programming semantics. In Kenneth A. Bowen and Robert A. Kowalski, editors, Proceedings of the Fifth International Conference/Symposium on Logic Programming, pages 1054–1069, Seattle, Washington, August 1988.

[HL94] P.M. Hill and J.W. Lloyd. The Gödel programming language. MIT Press, Cambridge, Massachusetts, 1994.

[Kun87] Kenneth Kunen. Negation in logic programming. Journal of Logic Programming, 4(4):289–308, December 1987.

[Llo84] John W. Lloyd. Foundations of logic programming. Springer series in symbolic computation. Springer-Verlag, New York, 1984.

[Llo87] J.W. Lloyd. Declarative error diagnosis. New Generation Computing, 5(2):133– 154, 1987.

[MO84] Alan Mycroft and Richard O’Keefe. A polymorphic type system for prolog. Artificial Intelligence, 23:295–307, 1984.

[Nai92] Lee Naish. Types and the intended meaning of logic programs. In Frank Pfenning, editor, Types in logic programming, pages 189–216. MIT Press, Cambridge, Massachusetts, 1992.

[Nai96] Lee Naish. A declarative view of modes. In Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming, pages 185–199. MIT Press, September 1996.

[Nai97a] Lee Naish. A declarative debugging scheme. Journal of Functional and Logic Programming, 1997(3), April 1997.

[Nai97b] Lee Naish. A three-valued declarative debugging scheme. Technical Report 97/5, Department of Computer Science, University of Melbourne, Melbourne, Australia, April 1997.

[PC88] Luis Moniz Pereira and Miguel Calejo. A framework for prolog debugging. In Kenneth A. Bowen and Robert A. Kowalski, editors, Proceedings of the Fifth International Conference/Symposium on Logic Programming, pages 481–495, Seattle, Washington, August 1988.

[Per86] Luis Moniz Pereira. Rational debugging in logic programming. In Ehud Shapiro, editor, Proceedings of the Third International Conference on Logic Programming, pages 203–210, London, England, July 1986. published as Lecture Notes in Computer Science 225 by Springer-Verlag.

[Sha83] Ehud Y. Shapiro. Algorithmic program debugging. MIT Press, Cambridge, Massachusetts, 1983.

[SHC95] Zoltan Somogyi, Fergus J. Henderson, and Thomas Conway. Mercury: an efficient purely declarative logic programming language. In Proceedings of the Australian Computer Science Conference, pages 499–512, Glenelg, Australia, February 1995.