10
Mathematical Aspects of Logic Programming Semantics
14
non-termination. These and other three-valued logics will be encountered
in Chapter 2 and in many other places in Chapters 3, 5, 6, and 7.
Fitting also considered Belnap’s four-valued logic
15 in which the truth set
is FOU R = {u, f , t, b}. Here, b denotes a fourth truth value intended to
represent both true and false, both or overdefined, which, it can be argued,
should be used to handle the conflicting information “both true and false”
returned, perhaps, in a distributed logic programming system. On a point of
notation, we remark that the listing of the elements in T W O corresponds to
the truth ordering ≤ t , as defined in Section 1.3.2, and in the case of T HREE
and FOU R the listing is derived from the knowledge ordering ≤ k , see again
Section 1.3.2, with incomparable elements listed alphabetically.
A fundamental concept throughout this work is that of valuation, or interpretation, and also that of model. Indeed, spaces of interpretations are one
of the central concepts here when viewed as the carrier sets for various semantic operators determined by programs. We will usually work later on in
the truth sets T W O and T HREE and sometimes in FOU R. Nevertheless, in
formulating the concepts of valuation and interpretation, we will work quite
generally, at no extra cost, and allow arbitrary sets of truth values and certain connectives defined on them. Thus, let T denote an arbitrary set of truth
values or truth set containing at least two elements, one of which will be the
distinguished value t, denoting true. We assume further that certain binary
connectives, namely, conjunction (∧) and disjunction (∨) are given, together
with a unary connective negation (¬), as functions over T . A third binary
connective implication (←) may also be given or it may be defined in terms
of the other connectives, and the latter is the way we will usually handle implication. However, we will defer giving the definition of implication we want
until we have dealt with orderings on truth sets, see Definition 1.3.3. A set
T together with specified definitions of these connectives will be referred to
as a logic and, when the definitions of the connectives are understood, will
be denoted simply by the underlying truth set T without causing confusion.
Quite often, the definitions of ∧, ∨, and ¬ are given by means of a truth
table, and this is the case for most of the logics we encounter here. For example, Table 1.1 specifies Belnap’s logic as employed by Fitting and by us.
It contains classical two-valued logic and Kleene’s strong three-valued logic
as sublogics.
16 Moreover, FOU R is a complete lattice, as we see later, and is
therefore technically easy to work with. Indeed, these are some of the reasons
why four-valued logic plays an important unifying role in the theory
17 and is
14 The truth value u is sometimes denoted in the literature by n, indicating none.
15 We refer to [Belnap, 1977, Fitting, 1991, Fitting, 2002], but note that Fitting worked
with a minor variant of the logic defined in [Belnap, 1977]; we work with this same variant
of Belnap’s definition.
16 The term a sublogic S of a logic T means that S is a subset of the set T of truth values,
and the connectives in S are restrictions to S of the corresponding connectives in T .
17 Fitting has shown the utility of FOU R, when viewed as a bilattice, in giving a unified
treatment of several aspects of logic programming, and we refer the reader to [Fitting, 2002]
and the works cited therein for more details.
Mathematical Aspects of Logic Programming Semantics
14
non-termination. These and other three-valued logics will be encountered
in Chapter 2 and in many other places in Chapters 3, 5, 6, and 7.
Fitting also considered Belnap’s four-valued logic
15 in which the truth set
is FOU R = {u, f , t, b}. Here, b denotes a fourth truth value intended to
represent both true and false, both or overdefined, which, it can be argued,
should be used to handle the conflicting information “both true and false”
returned, perhaps, in a distributed logic programming system. On a point of
notation, we remark that the listing of the elements in T W O corresponds to
the truth ordering ≤ t , as defined in Section 1.3.2, and in the case of T HREE
and FOU R the listing is derived from the knowledge ordering ≤ k , see again
Section 1.3.2, with incomparable elements listed alphabetically.
A fundamental concept throughout this work is that of valuation, or interpretation, and also that of model. Indeed, spaces of interpretations are one
of the central concepts here when viewed as the carrier sets for various semantic operators determined by programs. We will usually work later on in
the truth sets T W O and T HREE and sometimes in FOU R. Nevertheless, in
formulating the concepts of valuation and interpretation, we will work quite
generally, at no extra cost, and allow arbitrary sets of truth values and certain connectives defined on them. Thus, let T denote an arbitrary set of truth
values or truth set containing at least two elements, one of which will be the
distinguished value t, denoting true. We assume further that certain binary
connectives, namely, conjunction (∧) and disjunction (∨) are given, together
with a unary connective negation (¬), as functions over T . A third binary
connective implication (←) may also be given or it may be defined in terms
of the other connectives, and the latter is the way we will usually handle implication. However, we will defer giving the definition of implication we want
until we have dealt with orderings on truth sets, see Definition 1.3.3. A set
T together with specified definitions of these connectives will be referred to
as a logic and, when the definitions of the connectives are understood, will
be denoted simply by the underlying truth set T without causing confusion.
Quite often, the definitions of ∧, ∨, and ¬ are given by means of a truth
table, and this is the case for most of the logics we encounter here. For example, Table 1.1 specifies Belnap’s logic as employed by Fitting and by us.
It contains classical two-valued logic and Kleene’s strong three-valued logic
as sublogics.
16 Moreover, FOU R is a complete lattice, as we see later, and is
therefore technically easy to work with. Indeed, these are some of the reasons
why four-valued logic plays an important unifying role in the theory
17 and is
14 The truth value u is sometimes denoted in the literature by n, indicating none.
15 We refer to [Belnap, 1977, Fitting, 1991, Fitting, 2002], but note that Fitting worked
with a minor variant of the logic defined in [Belnap, 1977]; we work with this same variant
of Belnap’s definition.
16 The term a sublogic S of a logic T means that S is a subset of the set T of truth values,
and the connectives in S are restrictions to S of the corresponding connectives in T .
17 Fitting has shown the utility of FOU R, when viewed as a bilattice, in giving a unified
treatment of several aspects of logic programming, and we refer the reader to [Fitting, 2002]
and the works cited therein for more details.