9
Order and Logic
1.2.5 Definition The first-order language L given by an alphabet A consists
of the set of all well-formed formulae determined by the symbols of A. We refer
to terms over A as terms in or over L.
1.2.6 Example Suppose we are given an alphabet A containing constant
symbols a and b; variable symbols x and y; a unary function symbol f
and a binary function symbol g; and a unary predicate symbol p and a binary predicate symbol q. Then the following are examples of terms over A:
a, b, x, y, f (a), f (x), g(a, f (b)), g(g(a, b), f (y)), f (g(x, b)), . . .. In particular,
we note that, for example, f (a) and g(a, f (b)) are ground terms, whereas
f (g(x, b)) is not.
Furthermore, the following are examples of well-formed formulae in the
first-order language L determined by A: p(a), q(a, g(b, b)), ¬p(x), q(x, g(a, y)),
q(x, g(a, y))∨(p(y)∧¬p(x)), p(x) ← p(f (a))∧q(f (b), g(x, f (y)))∧q(x, g(y, b)),
p(x) ↔ q(f (x), g(x, x)), ∀x(p(x) ← p(a) ∧ ¬q(f (b), g(x, f (x))) ∧ q(x, g(x, b))).
In particular, the last of these is in a form of great significance in logic programming. Moreover, p(a) and q(a, g(b, b)), for example, are ground (atomic)
formulas, whereas ∀x∀y(p(x) ← p(a) ∧ ¬q(f (b), g(x, f (y))) ∧ q(x, g(y, b))) is
not ground.
1.2.2 Semantics of First-Order Predicate Logic
The definition formally describes the syntax of first-order predicate logic.
We want now, briefly, to describe formally the semantics or meaning given to
well-formed formulae. In doing this, we adopt the usual set-based approach
from model theory, but with two caveats which direct us. The first is that we
do need to handle more truth values than just the two conventional ones. The
second is that we do not usually need to handle quantified formulae because,
for purposes of the semantics of logic programs P , we usually consider the set
ground(P ), as defined in Chapter 2, instead of P itself, and elements of the
former contain no variable symbols and no quantifiers. However, in order to
proceed further it is necessary to discuss spaces of truth values, and we do
this next.
In classical two-valued logic and almost always in mathematics it is usual
to employ the set T W O = {f , t} of truth values false f and true t. However, in many places in logic programming and in other areas of computing, it has been found advantageous to employ more truth values than these.
Indeed, quite early on, Melvin Fitting argued in several places for the use
in logic programming of Kleene’s strong and weak three-valued logics, see
[Fitting, 1985, Fitting and Ben-Jacob, 1990], for example, in which the truth
set is T HREE = {u, f , t}. Here, f denotes false and t denotes true, again, but
u denotes a third truth value which may be thought of as representing underdefined, none (neither true nor false) or no information, or, in some contexts,
Précédent

- 40/305

Suivant