Interpretation
Interpretation: An interpretation of a first-order formula F is an assignment of values to each constant, functions symbol, and predicate symbol in F in a nonempty domain D according to the following rules:
1. An element in D is assigned to each constant.
2. A mapping Dn = {(x1, . . . , xn) | each xi ∈ D} to D is assigned to each n-place function symbol.
3. A mapping from Dn to {T,F} is assigned to each n-place predicate symbol. A formula can be evaluated to true or false given an interpretation over a domain D as follows:
1. The truth values of formulas involving P and Q with logical connectives are evaluated with the table in the previous section on propositional logic.
2. (∀x)P is T if the truth value of P is evaluated to T for every element in D; else F.
3. (∃x)P is T if the truth value of P is evaluated to T for at least one element in D; else F.
Example. Suppose we have the following formulas:
(∀x)IsAutomobile(x)
(∃x)¬IsAutomobile(x).
An interpretation is:
Domain: D = {MercedesBenzE320, HondaAccord, FordTaurus, Boeing777}. Assignment:
IsAutomobile(MercedesBenzE320) = T
IsAutomobile(HondaAccord) = T
IsAutomobile(FordTaurus) = T
IsAutomobile(Boeing777) = F
(∀x)IsAutomobile(x) is F in this interpretation
since IsAutomobile(x) is not T for x = Boeing777.
(∃x)¬IsAutomobile(x) is T in this interpretation
since ¬IsAutomobile(Boeing777) is T.
Closed Formula: A closed formula has no free occurrences of variables. The definitions for satisfiable formulas and valid formulas are similar to those for
propositional logic.
Satisfiable and Unsatisfiable Formulas: A formula G is satisfiable (consistent) iff there is at least one interpretation I in which G is evaluated to T. This interpretation I is said to satisfy G and is a model of G. A formula G is unsatisfiable (inconsistent) iff there is no interpretation I in which G is evaluated to T.
Valid Formula: A formula G is valid iff every interpretation of G satisfies G. To simplify proof procedures for first-order logic formulas, we first convert these formulas to standard forms discussed next.
Prenex Normal Forms and Skolem Standard Forms We now present a standard form introduced in [Davis and Putnam, 1960] for first-order logic formulas using prenex normal form, conjunctive normal form, and Skolem functions. This form will make it easier to mechanically manipulate and analyze logic formulas. A first-order logic formula can be converted into prenex normal form where all quantifiers are at the left end.
Prenex Normal Form: Formally, a formula F is in prenex normal form iff it is written in the form
(Q1v1) · · · (Qnvn)(M)
where every (Qivi ), i = 1, . . . , n, is either (∀vi ) or (∃vi ), and M is a formula with no quantifiers. (Q1v1) · · · (Qnvn) is the prefix and M is the matrix of F.
The matrix can be converted into a conjunctive normal form (CNF). The CNF prenex normal form can be converted into a Skolem standard form by removing the existential quantifiers using Skolem functions. This will simplify the proof procedures since existentially quantified formulas hold only for specific values.
The absence of existential quantifiers makes it trivially easy to remove the universal quantifiers as well.
Let Qi be an existential quantifier in the prefix (Q1v1) · · · (Qnvn), 1 ≤ i ≤ n. If there is no universal quantifier to the left of Qi , we replace all vi ’s in the matrix M by a new constant c distinct from the other constants in M, and remove (Qivi ) from the prefix. If (Qu1 · · · Qum ), 1 ≤ u1 < u2 · · · < um < i , are universal quantifiers to the left of Qi , we replace all vi in M by a new m-place function f (vu1, vu2, . . . , vum ) distinct from those in M and delete (Qi vi ) from the prefix. The resulting formula after removing all existential quantifiers is a Skolem standard form. The constants and functions used to replace the existential quantifiers are called Skolem constants and Skolem functions, respectively.
Example. Transform the following formula into a standard form:
(∃x)(∀y)(∀z)(∃u)(P(x, z, u) ∨ (Q(x, y)∧¬R(x, z))).
We first convert the matrix into a CNF:
(∃x)(∀y)(∀z)(∃u)((P(x, z, u) ∨ Q(x, y)) ∧ (P(x, z, u)∨¬R(x, z))).
Then we replace the the existential quantifiers with Skolem constants and functions. Starting from the leftmost existential quantifier, we replace its variable x by constant a:
(∀y)(∀z)(∃u)((P(a, z, u) ∨ Q(a, y)) ∧ (P(a, z, u)∨¬R(a, z))).
Next we use a 2-place function f (y, z) to replace the existential variable u:
(∀y)(∀z)((P(a, z, f (y, z)) ∨ Q(a, y)) ∧ (P(a, z, f (y, z))∨¬R(a, z))).
Proving Unsatisfiability of a Clause Set with Herbrand’s Procedure We can view propositional logic as a special case of predicate logic. By treating 0-place predicate symbols as atomic formulas of the propositional logic, predicate logic formulas become propositional logic formulas with no variables, function symbols, and quantifiers. Thus propositional logic formulas can be easily converted into corresponding predicate logic formulas.
However, we cannot in general reduce predicate logic formulas to single formulas of the propositional logic. However, we can systematically reduce a predicate
logic formula F to a countable set of formulas without quantifiers or variables. This collection of formulas is the Herbrand expansion of F, denoted by E(F).
A set S of clauses is unsatisfiable iff it is false under all interpretations over all domains. Unfortunately, we cannot explore all interpretations over all domains. However, there is a special domain called the Herbrand universe such that S is unsatisfiable iff S is false under all the interpretations over this domain. Herbrand Universe: The Herbrand universe of formula F is the set of terms built from the constant a and the function name f , that is, {a, f (a), f ( f (a)), . . .}. More formally, H0 = {a} if there is no constant in the set S of clauses; otherwise, H0 is the set of constants in S. Hi 1, i ≥ 0, is the union of Hi and the set of all terms of the form f n(x1, . . . , xn), each x j ∈ Hi , for all n-place functions f n in S. Hi is the i -level constant set of S, and H∞ is the Herbrand universe of S.
Example. S = {P(x) ∨ Q(x),¬R(y) ∨ T (y)∨¬T (y)}.
Since there is no constant in S, H0 = {a}. Since there is no function symbol in S,
H = H0 = H1 = · · · = {a}.