8
Mathematical Aspects of Logic Programming Semantics
bols
12 p, q, r, . . .. In addition, we have the connectives ¬, ∧, ∨, →, and ↔; the
quantifiers ∀ and ∃ ; and the punctuation symbols “(”, “)” and “, ”. The arity
of a function symbol f or of a predicate symbol p is commonly denoted by
#(f ) or by #(p).
In the following four definitions, we assume that A denotes some fixed,
but arbitrary, alphabet.
1.2.1 Definition We define a term (over ) A inductively
13 as follows.
(1) Each constant symbol in A is a term.
(2) Each variable symbol in A is a term.
(3) If f is any n-ary function symbol in A and t 1 , . . . , t n are terms, then
f (t 1 , . . . , t n ) is a term.
A term is called ground if it contains no variable symbols.
1.2.2 Definition An atom, atomic formula, or proposition A (over A) is an
expression of the form p(t 1 , . . . , t n ), where p is an n-ary predicate symbol in
A and t 1 , . . . , t n are terms (over A).
1.2.3 Definition A literal L is an atom A or the negation ¬A of an atom
A. Atoms A are sometimes called positive literals, and negated atoms ¬A are
sometimes called negative literals.
1.2.4 Definition A (well-formed ) formula (over A) is defined inductively as
follows.
(1) Each atom is a well-formed formula.
(2) If F and G are well-formed formulae, then so are ¬F , F ∧ G, F ∨ G,
F → G, and F ↔ G.
(3) If F is a well-formed formula and x is a variable symbol, then ∀xF and
∃xF are well-formed formulae also.
A well-formed formula is called ground if it contains no variable symbols.
Thus, in particular, a ground atom is an atom containing no variable symbols.
Of course, brackets are needed in writing down well-formed formulae to
avoid ambiguity. Their use can be minimized, however, by means of the customary precedence hierarchy (in descending order) in which ¬, ∀, ∃ have highest precedence, followed by that of ∨, followed next by the precedence of ∧,
and finally followed by → and ↔ with the lowest precedence.
12 Constant symbols, variable symbols, function symbols, and predicate symbols are sometimes referred to as simply constants, variables, functions, and predicates, respectively
13 As usual, in giving inductive definitions of sets, we omit the explicit statement of the
closure step and assume that what is being defined is the smallest set satisfying the basis
and induction steps.
Mathematical Aspects of Logic Programming Semantics
bols
12 p, q, r, . . .. In addition, we have the connectives ¬, ∧, ∨, →, and ↔; the
quantifiers ∀ and ∃ ; and the punctuation symbols “(”, “)” and “, ”. The arity
of a function symbol f or of a predicate symbol p is commonly denoted by
#(f ) or by #(p).
In the following four definitions, we assume that A denotes some fixed,
but arbitrary, alphabet.
1.2.1 Definition We define a term (over ) A inductively
13 as follows.
(1) Each constant symbol in A is a term.
(2) Each variable symbol in A is a term.
(3) If f is any n-ary function symbol in A and t 1 , . . . , t n are terms, then
f (t 1 , . . . , t n ) is a term.
A term is called ground if it contains no variable symbols.
1.2.2 Definition An atom, atomic formula, or proposition A (over A) is an
expression of the form p(t 1 , . . . , t n ), where p is an n-ary predicate symbol in
A and t 1 , . . . , t n are terms (over A).
1.2.3 Definition A literal L is an atom A or the negation ¬A of an atom
A. Atoms A are sometimes called positive literals, and negated atoms ¬A are
sometimes called negative literals.
1.2.4 Definition A (well-formed ) formula (over A) is defined inductively as
follows.
(1) Each atom is a well-formed formula.
(2) If F and G are well-formed formulae, then so are ¬F , F ∧ G, F ∨ G,
F → G, and F ↔ G.
(3) If F is a well-formed formula and x is a variable symbol, then ∀xF and
∃xF are well-formed formulae also.
A well-formed formula is called ground if it contains no variable symbols.
Thus, in particular, a ground atom is an atom containing no variable symbols.
Of course, brackets are needed in writing down well-formed formulae to
avoid ambiguity. Their use can be minimized, however, by means of the customary precedence hierarchy (in descending order) in which ¬, ∀, ∃ have highest precedence, followed by that of ∨, followed next by the precedence of ∧,
and finally followed by → and ↔ with the lowest precedence.
12 Constant symbols, variable symbols, function symbols, and predicate symbols are sometimes referred to as simply constants, variables, functions, and predicates, respectively
13 As usual, in giving inductive definitions of sets, we omit the explicit statement of the
closure step and assume that what is being defined is the smallest set satisfying the basis
and induction steps.