Transcript Folie 1 - STI Innsbruck

Intelligent Systems
Lecture III – xx 2009
Predicate Logic
Dieter Fensel and Dumitru Roman
©www.sti-innsbruck.at
Copyright 2008 STI INNSBRUCK www.sti-innsbruck.at
Where are we?
#
Date
Title
1
Introduction
2
Propositional Logic
3
Date
Predicate Logic
4
Theorem Proving, Logic Programming, and Description Logics
5
Search methods
6
CommonKADS
7
Problem-Solving Methods
8
Planning
9
Agents
10
Rule learning
11
Inductive Logic Programming
12
Formal Concept Analysis
13
Neural Networks
14
Semantic Web and Exam Preparation
www.sti-innsbruck.at
2
Outline
• Motivation
• Technical Solution
– Formulas, Models, Tableaux
– Deductive Systems
– Resolution
•
•
•
•
Illustration by Larger Examples
Extensions
Summary
References
Note: Most of the content of this lecture is based on Chapters 5-7 of the book
Mathematical Logic for Computer Science (by Mordechai Ben-Ari)
http://www.springer.com/computer/foundations/book/978-1-85233-319-5
www.sti-innsbruck.at
3
MOTIVATION
www.sti-innsbruck.at
4
Predicate logic
•
Propositional logic is not expressive enough
– Suppose we want to capture the knowledge that
Anyone standing in the rain will get wet.
and then use this knowledge. For example, suppose we also learn that
Jan is standing in the rain.
– We'd like to conclude that Jan will get wet. But each of these sentences would
just be a represented by some proposition, say P, Q and R. What relationship is
there between these propositions? We can say
P /\ Q → R
Then, given P /\ Q, we could indeed conclude R. But now, suppose we were told
Pat is standing in the rain.
– We'd like to be able to conclude that Pat will get wet, but nothing we have stated
so far will help us do this
– The problem is that we aren't able to represent any of the details of these
propositions. It's the internal structure of these propositions that make the
reasoning valid. But in propositional calculus we don't have anything else to talk
about besides propositions!
 A more expressive logic is needed
 Predicate logic (occasionally referred to as First-order logic)
www.sti-innsbruck.at
5
TECHNICAL SOLUTION
www.sti-innsbruck.at
6
Predicate Logic – Overview
• All the logical machinery – formulas, interpretations, proofs, etc. –
that was developed for the propositional logic (see previous lecture)
can be applied to predicates
– The presence of a domain upon which predicates are interpreted
considerably complicates the technical details but not the basic
concepts
• Syntax
– Predicate symbols are used to represent relations (functions from a
domain to truth values)
– Quantifiers allow a purely syntactical expression of the statement that
the relation represented by the predicate is true for some or all elements
of the domain
• Semantics
– An interpretation consists of a domain and an assignment of relations to
the predicate letters
– The semantics of the Boolean operators remains unchanged, but the
evaluation of the truth value of the formula must take the quantifiers into
account
www.sti-innsbruck.at
7
Predicate Logic – Overview (cont’)
• Semantic tableaux
– The systematic search for a model is potentially infinite because
the domains like the integers are infinite
– The construction of a tableau may not terminate, so there is no
decision procedure for satisfiability in the predicate logic,
however, if a tableau happens to close, the formula is
unsatisfiable, conversely, a systematic tableau for an
unsatisfiable formula will close
• There are Gentzen and Hilbert deductive systems which
are sound and complete
– A valid formula is provable and we can construct a proof of the
formula using tableaux, but given an arbitrary formula we cannot
decide if it is valid and hence provable
www.sti-innsbruck.at
8
Predicate Logic – Overview (cont’)
• The syntax of predicate logic is extended with function
symbols that are interpreted as functions on the domain
– The predicate logic with function symbols is used in the
resolution procedure
• There are canonical interpretations called Herbrand
interpretations
– If a formula has a model, it has a model which is an Herbrand
interpretation, so to check satisfiablity, it is sufficient to check if
there is a Herbrand model for a formula
www.sti-innsbruck.at
9
Predicate Logic – Formulas, Models, Tableaux
•
•
•
•
•
•
•
Relations and Predicates
Predicate Formulas
Interpretations
Equivalence and Substitution
Semantic Tableaux
Finite and Infinite Models
Undecidability of the Predicate Logic
www.sti-innsbruck.at
10
Relations and Predicates
• The axioms and theorems of mathematics are defined
on arbitrary sets such as the set of integers
– We need to be able to write and manipulate logical formulas that
contain relations on values from arbitrary sets
• The predicate logic extends the propositional logic with
predicate symbols that are interpreted as relations on a
domain
• Let R be an n-ary relation on a domain D, i.e. R is a
subset Dn. A relation can be represented by a Booleanvalued function R: Dn → {T,F}, by mapping an n-tuple to
T iff it is included in the relation:
R(d1,…,dn) = T iff in R(d1,…,dn) in R
www.sti-innsbruck.at
11
Predicate Formulas
•
•
•
Predicate (relation) symbols
Constant symbols
Variables
•
BNF Grammar for Predicate Formulas:
www.sti-innsbruck.at
12
Predicate Formulas (cont’)
• Examples:
• Suppose A is a predicate formula. An occurrence of a variable x in A
is a free variable of A if it is not within the scope of any quantifier
A variable which is not free is said to be bound
• Examples:
www.sti-innsbruck.at
13
Interpretations
• Let U be a set of formulas such that {p1, p2, . . . , pm} are
all predicate symbols appearing in U and {a1, a2, . . . , ak}
are all constant symbols appearing in U. An
interpretation I of U is a tripe
I = (D, {R1,…,Rm}, {d1,…,dk})
where
– D is a non-empty set (domain of I)
– Ri is an assignment of an ni-ary relation on D to the ni-ary
predicate symbol pi
– di is an assignment of an element of D to the constant ai
www.sti-innsbruck.at
14
Interpretations (cont’)
•
Example: Consider the formula
Some of its possible interpretations are:
“For every natural number x, 0 ≤ x.”
“For every natural number x, 1|x.”
“For every string x over alphabet {0, 1}, empty string is a substring of
x.”
“For every vertex x of G, (a, x) is an edge in G.”
www.sti-innsbruck.at
15
Interpretations (cont’)
•
•
Suppose I is an interpretation for a predicate formula A. An assignment
is a function which assigns a value in the domain D to any variable
appearing in the formula A
Suppose A is formula, I an interpretation for A, and σI an assignment. We
define vσI(A), the truth value of A under σI, inductively:
(a) If A = p(c1, c2,…, cn) is an atomic formula, where each ci is either a
variable xj or a constant symbol aj, then
(b) vσI(¬A) = ¬vσI (A)
(c) vσI(A1 /\ A2) = vσI (A1) /\ vσI (A2)
(d) vσI(A1 \/ A2) = vσI (A1) \/ vσI (A2)
(e)
(f)
www.sti-innsbruck.at
16
Interpretations (cont’)
• Theorem: If A is a closed formula, then vσI(A) does not
depend on σI. In that case, we write vI(A).
• Theorem: Let A' = A(x1, x2, . . . , xn) be a non-closed
formula and let I be an interpretation. Then:
(a) vσI(A) = T for assignment σI iff
(b) vσI(A) = T for all assignments σI iff
www.sti-innsbruck.at
17
Interpretations (cont’)
• A closed formula A is true in I, or I is a model for A, if
vI(A) = T
I |= A
• A closed formula A is satisfiable if, for some
interpretation I,
I |= A
• A is valid if, for all interpretations I,
I |= A
• A is unsatisfiable if it is not satisfiable, and falsifiable if it
is not valid
www.sti-innsbruck.at
18
Interpretations (cont’)
• Examples:
www.sti-innsbruck.at
19
Equivalence and Substitution
• Suppose A1,A2 are two closed formulas. If, for all
interpretations I
vI(A1) = vI(A2)
we say that A1 and A2 are equivalent, and we write
A1 ≡ A2
• Suppose U is a set of closed formulas, and A a closed
formula
U |= A
means that, in all interpretations I in which all formulas
from U are true, we also have
vI(A) = T
• Examples:
www.sti-innsbruck.at
20
Equivalence and Substitution (cont’)
• Theorem:
A ≡ B iff |= A ↔ B
U |= A iff |= A1 /\ A2 /\ ... /\ An → A
• Examples of valid formulas:
www.sti-innsbruck.at
21
Semantic Tableaux
• Recall that a tableaux is systematic search for a counter
example
• Example: We will try to show that
is a valid formula.
We consider its negation
and try to show that it is unsatisfiable.
www.sti-innsbruck.at
22
Semantic Tableaux (cont’)
• Semantic tableaux for
www.sti-innsbruck.at
:
23
Semantic Tableaux (cont’)
• Example: Now, consider the formula
which is satisfiable but not valid (so its negation should also be
satisfiable). Semantic tableaux (we obtain a closed tableau for a
satisfiable formula):
www.sti-innsbruck.at
24
Semantic Tableaux (cont’)
• Question: What went wrong in the previous example?
– The same constant a was used twice to eliminate two distinct existential
quantifiers
– We were forced to use the same constant since, once we eliminated the
universal quantifier in
we replaced it with a and were forced to work with that constant
exclusively from that point on
• Solution: We will not delete universal quantifiers from nodes of the
tableau; instead, we introduce some instance of that variable but
keep writing the universal quantifier. E.g.
www.sti-innsbruck.at
25
Semantic Tableaux (cont’)
• Using these guidelines, if a tableau for the formula from
the previous example is correctly constructed, one
branch ends with the open leaf
In fact, this leaf gives a model for this satisfiable formula;
the domain is
D = {a, b}
and the unary relations are subsets
p = {a},
q = {b}
(This is what we will be defined as an Herbrand model
for this formula later on in this lecture)
www.sti-innsbruck.at
26
Semantic Tableaux (cont’)
• Example: Consider the formulas
Check whether A = A1 /\ A2 /\ A3 is a satisfiable formula and, if so,
find one model for A.
Solution: First construct a semantic tableau for the formula:
www.sti-innsbruck.at
27
Semantic Tableaux (cont’)
•
•
The tableau in the previous example does not terminate; namely, every time
an universal or an existential quantifier is dropped, a new constant symbol
ai can be introduced, to get an infinite sequence of constants:
a1, a2,…, an,…
The formula does have an obvious infinite model:
I = (N, {<})
Furthermore, one can prove, using the formulas A2 and A3 (see the proof of
Theorem 5.24 in the textbook) that every model of
A = A1 /\ A2 /\ A3
must be infinite. So, the tableau construction effectively produces a
“generic” infinite model for A.
One major difference in comparison with semantic tableaux for
propositional logic is (as seen in the previous example) that a tableau of a
predicate formula may not terminate
– The reason for this anomaly is that, in propositional logic, nodes of a tableau
simplify in terms of the formula complexity. In predicate logic, this is not the case,
since we can never eliminate universal quantifiers
www.sti-innsbruck.at
28
Semantic Tableaux - Algorithm for Semantic
Tableaux
• As in propositional case, we generalize the rules into two
cases, γ-rules for universal formulas and δ-rules for existential
formulas:
• A literal is a closed atomic formula p(a1, a2,…, an) or the
negation of such a formula
• Algorithm for construction of a semantic tableau:
Input: A predicate formula A
Output: Semantic tableau T for A; all branches are either
infinite, or finite with leaves marked × (closed) or o (open).
A semantic tableau is a tree T each node of which will be
labeled with a set of formulas. T is built as follows.
www.sti-innsbruck.at
29
Semantic Tableaux - Algorithm for Semantic
Tableaux (cont’)
(1) Initially, T is a single node, labeled {A}
(2) We build the tableau inductively by choosing an unmarked leaf l,
labeled U(l), and applying one of the following rules:
– If U(l) is a set of literals and γ -formulas containing a pair of
complementary literals {p(a1, a2,…, an), ¬p(a1, a2,…, an)}, mark it as
closed (×)
– If U(l) is not a set of literals, choose a formula A in U(l) which is not a
literal:
• α- and β-rules are applied just as in propositional logic
• If A is a γ-formula, add a new node l', a child of l, and label it
U(l') = U(l) U {γ(a)}
where a is a constant appearing in U(l). If U(l) consists of literals
and γ -formulas only, mark it × or o, depending on whether there is a
set of complementary literals.
• If A is a δ-formula, create a new node l' as a child of l and label it
U(l') = (U(l) − {A}) U {δ(a)}
where a is some constant that does not appear in U(l).
www.sti-innsbruck.at
30
Semantic Tableaux - Algorithm for Semantic
Tableaux (cont’)
• A branch in T is closed if it terminates in a leaf marked ×.
Otherwise, it is open.
• Theorem (Soundness): Suppose A is a predicate formula
and T its semantic tableau. If T closes, then A is
unsatisfiable.
• Theorem (Completeness): Suppose A is a valid formula.
Then, the systematic semantic tableau for A terminates
and is closed.
(Note: see section 5.5 in the textbook for a detailed description of
systematic semantic tableau)
www.sti-innsbruck.at
31
Finite and Infinite Models
• Theorem (Löwenheim): If a formula is satisfiable, then it
is satisfiable in a countable model
• Theorem (Löwenheim - Skolem): If a countable set of
predicate formulas is satisfiable, then it is satisfiable in a
countable model
• Theorem (Compactness Theorem): Let U be a countable
set of formulas. If all finite subsets of U are satisfiable,
then so is U
www.sti-innsbruck.at
32
Undecidability of the Predicate Logic
• Church, building on the work of Turing, proved that there is no
decision procedure for validity in predicate logic
• Turing machines can be viewed as devices which compute functions
on natural numbers; i.e. given a Turing machine T, we can associate
to it a function
fT : N → N
so that fT(n) = m if T halts with the tape consisting of m 1’s when
started on the tape with the input of n consecutive 1’s. If T never
halts on the input of n consecutive 1’s, then fT(n) is undefined
• Theorem (Church): It is undecidable whether a Turing machine,
started on a blank tape, will halt
– In other words, it is undecidable, given a Turing machine T, whether fT
(0) is defined
www.sti-innsbruck.at
33
Undecidability of the Predicate Logic (cont’)
• Two-register machine (or, a Minsky machine) M consists of a pair of
registers (x, y) which can store natural numbers, and a program P =
{L0, L1,…, Ln}, which is a sequential list of instructions. Ln is always
the command “halt”, and for 0 ≤ i < n, Li has one of the two forms
– r := r + 1, for r in {x, y}
– if r = 0 then go to Lj else r := r − 1, for r in {x, y}, 0 ≤ j ≤ n
• Execution of M: sequence of states sk = (Li , x, y) where Li is the
current instruction during the execution, and x,y are current contents
of the two registers.
– Initial state: s0 = (L0,m, 0), for some m
– If sk = (Ln, x, y), for some k then M halts and y = f (m) is computed by M
• Theorem: For every Turing machine T that computes f : N → N, a
two-register machine M can be constructed which computes the
same function.
– Corollary: It is undecidable whether, given a two-register machine M,
whether fM(0) exists or not
www.sti-innsbruck.at
34
Undecidability of the Predicate Logic (cont’)
• Theorem (Church): Validity in predicate calculus is undecidable
Sketch of the Proof:
To each two-register machine M, we associate a predicate formula
SM such that M halts when started at (L0, 0, 0)  |= SM
We use the language:
– Binary relations: pi (x, y) (i = 0, 1,…, n)
– Unary function: s(x)
– Constant symbol: a
Intended interpretation:
– pi (x, y): M is at the state (Li, x, y)
– s(x): successor function s(x) = x + 1
– a: a = 0
www.sti-innsbruck.at
35
Undecidability of the Predicate Logic (cont’)
Finally, define
SM says the following: if a machine with the program P = {L0, L1, . . . ,
Ln} is started at the initial state (L0, 0, 0), then the computation will
halt with the values at the registers being (z1, z2), for some natural
numbers z1, z2
Si is defined by cases of the instruction Li :
Since the Halting Problem for two-register machines is undecidable,
it is impossible to verify algorithmically whether |= SM or not.
www.sti-innsbruck.at
36
Predicate Calculus: Deductive Systems
• Gentzen System G
• Hilbert System H
www.sti-innsbruck.at
37
Gentzen System G
• As in propositional logic, Gentzen proof system is based on the
reversal of a semantic tableau for a formula
• Example: Prove that
Solution: start by constructing a tableau for the negation
:
www.sti-innsbruck.at
38
Deductive System G
• Axioms: Any set of formulas U containing a
complementary pair of literals
• Rules: α- and β-rules are the same as in propositional
logic, plus
where
and a is an arbitrary constant.
• Theorem (Soundness and Completeness) Let U be a set
of formulas. There is a Gentzen proof for U if and only if
there is a closed semantic tableau for U.
www.sti-innsbruck.at
39
Deductive System G
• Example: The proof in G for
is
www.sti-innsbruck.at
40
Hilbert System H
• Axioms: The three axioms for the Hilbert system
in propositional logic, plus
– Axiom 4.
– Axiom 5.
assuming x is not free in A
• Rules of Inference: Modus Ponens, plus
(Generalization:)
www.sti-innsbruck.at
41
Hilbert System H (cont’)
• There is a problem with the Generalization Rule if it is not being
used judiciously; consider the following derivation in the set N with
the unary predicate even(x):
1. even(2) ├ even(2)
2. even(2) ├ even(x)
Assumption
Gen. Rule 1
We derived a wrong conclusion that every natural number is even,
starting from the true assumption that 2 is even. What went wrong?
Answer: We should not be able to generalize based on a constant
included in the assumptions. Namely, assumptions may contain very
specific facts and not simply general logical truths.
The Generalization Rule must be modified as follows (and with the
modification the deduction rule can be further defined)
www.sti-innsbruck.at
42
Hilbert System H (cont’)
• Generalization Rule:
provided a does not appear in U.
• Deduction Rule:
• Theorem (Soundness and Completeness): Hilbert proof system H
for predicate logic is sound and complete.
• Axiom 4 and MP justify the following derived rule
(Specification Rule):
for any constant a.
www.sti-innsbruck.at
43
Some relevant theorems and proofs in H
• Theorem:
Proof:
• Theorem:
Proof:
www.sti-innsbruck.at
44
Some relevant theorems and proofs in H (cont’)
• Theorem:
Proof:
• This proves a more general version of the Generalization
Rule:
www.sti-innsbruck.at
45
Some relevant theorems and proofs in H (cont’)
• Theorem:
Proof:
• Theorem:
Proof:
www.sti-innsbruck.at
46
Resolution
•
•
•
•
•
•
•
•
Functions and Terms
Clausal Form
Herbrand Models
Herbrand’s Theorem
Ground Resolution
Substitutions
Unification
General Resolution
www.sti-innsbruck.at
47
Functions and Terms
• We will now allow the language for predicate logic to
contain function symbols; they will be interpreted as
functions (of appropriate arity) in the domain of an
interpretation
• Example: Consider the formula p(x, y) → p(x, f (y))
where p is a binary predicate symbol, and f is a unary
function symbol; two possible interpretations of this
formula
– I1 = (N, {<}, {succ(x)}), where succ(x) = x + 1
– I2 = ({0, 1}*, {substr}, {f }), where the relation substr(w1,w2) means
that w1 is a substring of w2, and f(w) = w0, is the function
appending 0 to the right end of word w
www.sti-innsbruck.at
48
Functions and Terms (cont’)
• Terms: Suppose
then
• Suppose a, b are constant symbols, p a binary predicate symbol, f is
a binary function symbol, and g a unary function symbol
– Examples of terms: a, g(a), f (x, y), f (x, g(a)), f (f (a, x), b), f (f (x, y), f (b,
g(a))),…
– Examples of atomic formulas: p(a, a), p(f (x, y), g(y)), p(g(b), f (a,
g(a))),…
www.sti-innsbruck.at
49
Functions and Terms (cont’)
• A term or atom is ground if it contains no variables; a
formula is ground if it has no quantifiers and no variables
• A' is a ground instance of a quantifier-free formula A if it
can be obtained from A by substituting ground terms for
free variables
• Examples:
– Examples of ground terms: f(a, a), g(b), f(f (a, b), g(a)),…
– Examples of ground formulas: ¬p(a, a), p(f (a, b), b) → p(a, a),…
– The formula ¬p(f(a, b), b) \/ p(a, f(a, a)) is a ground instance of
the formula ¬p(f(x, b), y) \/ p(x, f(x, x))
www.sti-innsbruck.at
50
Clausal Form
• A formula A is in prenex conjunctive normal form
(PCNF), iff it is of the form
Q1x1Q2x2…Qnxn M(x1, x2,..., xn)
where Qi (i = 1, 2,…, n) are quantifiers and M(x1, x2,...,
xn) is a quantifier-free formula in CNF, called the matrix
of A.
• A closed formula is in clausal form if it is in PCNF and
all quantifiers Qi are universal.
• A literal is an atomic formula or its negation; e.g.
p(x, f(a, y)),¬p(g(x), f(x, g(x)))
A literal is said to be ground if it contains no variables.
A clause is a disjunction of literals; e.g.
¬p(x, y) \/ p(x, f (x))
www.sti-innsbruck.at
51
Clausal Form (cont’)
• C' is a ground clause if it is a ground instance of a clause C; e.g. if
C = ¬p(x, y) \/ p(x, f (x)),
the substitution x ← f(a), y ← a produces the ground clause
C' = ¬p(f(a), a) /\ p(f(a), f(f(a)))
• Example of formula in clausal form:
This clausal form can be written in the following way:
{{p(x, f(y)), q(z)}, {¬q(f(x)),¬p(f(y), z)}}
An even more simplified version of this clausal form is:
{pxfyqz,¬qfx¬pfyz}
www.sti-innsbruck.at
52
Clausal Form (cont’)
• The notation A ≈ B is used to denote the fact that a formula A is
satisfiable iff B is satisfiable
• Theorem (Skolem): Suppose A is a closed formula. Then, there
exists a formula A' in clausal form such that
A ≈ A‘
Proof (Algorithm for converting A to A'):
We start with a particular formula
and we will illustrate each step of the algorithm by showing how it
applies to this particular example
Input: Closed formula A
Output: formula A' in clausal form, such that A ≈ A‘
The following steps are performed (see next slide)
www.sti-innsbruck.at
53
Clausal Form (cont’)
(1) Rename bound variables (if necessary) so that no
variable appears in the scope of two different
quantifiers:
(2) Eliminate all propositional connectives, except for
negation, conjunction, and disjunction
(3) Push all negations inward and eliminate double
negations:
(4) Extract quantifiers from the matrix:
www.sti-innsbruck.at
54
Clausal Form (cont’)
(5) Transform the matrix of the formula into CNF:
(6) Eliminate existential quantifiers:
– If we have
replace x with a new constant symbol a
– If we have
, replace y with f(x1, x2, .
. . , xn), where f is a new n-ary function symbol
• The method of converting a closed formula A into a
clausal form A' so that A ≈ A‘ is also called Skolemization
of A
www.sti-innsbruck.at
55
Clausal Form (cont’)
• Example: Transform the formula
into a clause form A' ≈ A
Solution:
www.sti-innsbruck.at
56
Herbrand Models
• Once we allow function symbols in the language
of predicate logic, the models can become
rather complicated since, given any function
symbol, there are a large number of functions on
the domain that can interpret it
• We will show that, if a set of clauses has a
model (i.e. is satisfiable), it has a particular
canonical (or, generic) model
www.sti-innsbruck.at
57
Herbrand Models (cont’)
• Let S be a set of clauses and
–
–
: set of constant symbols appearing in S
: set of function symbols appearing in S
• We define HS, the Herbrand universe HS for S is defined
inductively, as follows:
– a HS, for every a
– f(t1, t2,…, tn), for every n-ary function symbol f
and (t1, t2,…, tn) HS
,
If there are no constant symbols in S ( = Ø), we
initialize the inductive definition by putting some arbitrary
new constant symbol a in HS.
• Remark: The Herbrand universe HS for S will be infinite
as soon as there is a function symbol in S
www.sti-innsbruck.at
58
Herbrand Models (cont’)
• Examples:
– If S1 = {pxy¬qa, qa¬pbx}, then
HS = {a, b}
– If S2 = {¬pxf (y), pwg(w)}, then
HS = {a, f(a), g(a), f(f(a)), f(g(a)), g(f(a)), g(g(a)),…}
– If S3 = {¬paf (x, y), pbf (x, y)}, then
HS = {a, b, f(a, a), f(a, b), f(b, a), f(b, b), f(a, f(a, a)),
f(f(a, a), a),…}
www.sti-innsbruck.at
59
Herbrand Models (cont’)
• Suppose HS is the Herbrand universe for a set of clauses. The
Herbrand base BS is the set of ground atomic formulas formed using
the predicate symbols in S and terms from HS.
• Example:
– For S3 = {¬paf (x, y), pbf (x, y)}, the Herbrand base is
BS = {p(a, f(a, a)), p(a, f(a, b)), p(a, f(b, a)), p(a, f(b, b)), …, p(a, f(f(a, a),
a)), . . . , p(b, f(a, a)), p(b, f(a, b)), p(b, f(b, a), p(b, f(b, b))
• An Herbrand model for a set of clauses S consists of the Herbrand
universe HS as the domain, the function symbols and constants are
interpreted by themselves, and the relations are interpreted in some
way which would make all the clauses in S true; in other words, the
true relations form some subset of BS which makes all clauses true
www.sti-innsbruck.at
60
Herbrand Models (cont’)
• Example:
For S3 = {¬paf(x, y), pbf(x, y)}, the Herbrand universe is
HS = {a, b, f(a, a), f(a, b), f(b, a), f(b, b), f(a, f(a, a)), f(f(a, a), a),…}
The relations in Herbrand model are given as
v(p(a, f(a, a))) = F, v(p(a, f(b, a))) = F, v(p(a, f(a, b))) = F
v(p(a, f(b, b))) = F,
v(p(b, f(a, a))) = T, v(p(b, f (b, a))) = T,
v(p(b, f(a, b))) = T, v(p(b, f(b, b))) = T, …
• Theorem: Let S be a set of clauses. S has a model if and
only if it has an Herbrand model.
www.sti-innsbruck.at
61
Herbrand Models (cont’)
• Theorem (Herbrand’s Theorem - Semantic Form): A set of clauses S
of predicate logic is unsatisfiable if and only if a finite set of ground
instances of clauses from S is unsatisfiable
• Example: Consider the following unsatisfiable formula
Its clausal form is {¬p(x) \/ q(x), p(y),¬q(z)}
One set of ground instances for this set of clauses is:
{¬p(a) \/ q(a), p(a),¬q(a)}
obtained by substitution x ← a, y ← a, z ← a
Now, we can use any method for proving unsatisfiability from
propositional logic (semantic tableaux, resolution, etc.):
www.sti-innsbruck.at
62
Herbrand Models (cont’)
•
Herbrand’s theorem gives us the handle needed to
define an efficient semi-decision procedure for validity
of formulas in the predicate calculus:
1.
2.
3.
4.
Negate the formula
Transform the formula into a clausal form
Generate a finite set of ground instances of clauses
Check if the set of ground clauses from (3) is unsatisfiable
Step 3 is highly problematic; namely, there are infinitely many
ground terms (if there is at least one function symbol) so it may
be difficult to find a correct substitution for resolution. In fact, if
the set of clauses is satisfiable, there is no such substitution, so
our search for it may run forever. This is not surprising,
however, considering that we already know that the validity in
predicate logic is undecidable.
www.sti-innsbruck.at
63
Ground Resolution
• Suppose C1,C2 are ground clauses containing a pair of
clashing literals l, lc , say, l in C1, lc in C2. The resolvent of
C1 and C2 is the clause
C1 and C2 are called the parent clauses in resolution
• Theorem: The resolvent C is satisfiable if and only if C1
and C2 are simultaneously satisfiable
www.sti-innsbruck.at
64
Substitutions
• Suppose x1, x2,..., xn are distinct variables and t1, t2,…, tn terms such
that ti is not equal to xi (i = 1, 2,…, n). The substitution
{x1 ← t1, x2 ← t2,…, xn ← tn}
is the mapping assigning the term ti to the variable xi.
– Generally, we will use Greek letters Θ, σ, ζ, μ,… to denote substitutions
• An expression is any term, literal, a clause, or a set of clauses. If E
is an expression and
σ = {x1 ← t1, x2 ← t2,…, xn ← tn}
is a substitution, the instance Eσ is obtained by simultaneously
applying the substitution σ to all occurrences of xi’s in E
• Example: Suppose the expression E is the clause p(x, y) \/ ¬q(f(x))
and σ is the substitution {x ← a, y ← f(x)}. Then the instance Eσ of E
is:
Eσ = p(a, f(x)) \/ ¬q(f(a))
www.sti-innsbruck.at
65
Substitutions (cont’)
• Suppose
Θ = {x1 ← t1, x2 ← t2,…, xn ← tn}
σ = {y1 ← s1, y2 ← t2,…, yk ← sk}
are two substitutions with X = {x1, x2,..., xn }, Y = {y1, y2,..., yk}.
The composition of Θ and σ is the substitution
Θσ = {xi ← tiσ : xi ≠ tiσ} U {yj ← sj : yj in Y, yj not in X}
In plain English: first apply the substitution σ to the terms ti that
appear in Θ. If some substitutions become xi ← xi, delete them.
Finally, append all yj ← sj to the list, for which yj is not one of the
variables xi in Θ.
• Lemma: If E is an expression and Θ and σ are two substitutions,
E(Θσ) = (EΘ)σ
• Lemma: The composition of substitutions is associative: if Θ, σ, and
ζ are substitutions,
Θ(σζ) = (Θσ)ζ
www.sti-innsbruck.at
66
Unification
• Consider the pair of literals
p(f (x), g(y)),
¬p(f(f(a)), g(z)).
This pair cannot be resolved using the method of ground resolution.
However, the substitution
{x ← f(a), y ← a, z ← a}
will turn the pair into
p(f(f(a)), g(a)), ¬p(f(f(a)), g(a))
to which ground resolution can be applied.
In fact, a simpler substitution
{x ← f(a), y ← z}
will also accomplish this, even though we will not end up with a pair
of ground literals, but
p(f(f(a)), g(z)), ¬p(f(f(a)), g(z)),
which are still clashing.
www.sti-innsbruck.at
67
Unification (cont’)
• Given a set of atoms, a unifier is a substitution which
makes the atoms identical. A most general unifier, or
m.g.u, for short, is a unifier μ such that, if Θ is any unifier
for the set of atoms
Θ=μζ
for some substitution ζ.
In other words, every unifier for that set of atoms can be
obtained from an m.g.u. through further substitution.
• Example: The unifier
μ = {x ← f(a), y ← z}
is an m.g.u. for the set of atoms p(f(x), g(y)) and p(f(f(a)),
g(z)). In fact,
{x ← f(a), y ← a, z ← a} = μ{z ← a}
www.sti-innsbruck.at
68
Unification (cont’)
•
Question: When is it impossible to unify two atomic
formulas?
1. if they start with different predicate symbols (obvious)
2. A trickier obstacle: consider the pair of atoms
p(a, x), p(a, f(x))
No matter what substitution we attempt to use, the problem is that
we will never be able to make the terms x and f(x) identical.
The reason for this is that the two terms we are attempting to unify
contain the same variable.
www.sti-innsbruck.at
69
Unification (cont’)
•
•
If we want to unify two atoms
p(t1, t2,…, tn), p(t’1, t’2,…, t’n)
we are trying to unify pairs of terms t1 and t’1 , t2 and t’2,…, tn and t’n.
We can view this problem as attempting to solve a system of n term
equations:
t1 = t’1
t2 = t’2
...
tn = t’n
Example: The problem of trying to unify the pair of atoms
p(x, f(y)), p(f(f(y)), g(a))
can be viewed as solving the system of two term equations:
x = f(f(y))
f(y) = g(a)
Based on the above remark, this system cannot be solved since the terms
in the second equation start with different function symbols
www.sti-innsbruck.at
70
Unification (cont’)
• A set of term equations is in solved form if:
– All equations are of the form
x = t, x − variable , t − term not containing x
– Every variable x which appears in the left-hand side of one of the
equations does not appear in any other equation in the system.
If the solved form of the system is
x1 = t1, x2 = t2,…, xn = tn
the solving substitution is
σ = {x1 ← t1, x2 ← t2,…, xn ← tn}
www.sti-innsbruck.at
71
Unification Algorithm
Input: A set of term equations
Output: A set of term equations in solved form or the answer “not
unifiable”
(1) Transform every equation of the form t = x (x-variable, t-term which
is not a variable) into x = t;
(2) Delete all trivial equations of the form x = x (x-variable)
(3) Suppose t' = t'' is an equation where neither term t', t'' is a variable.
If starting function symbols of t' and t'' are not the same, output “not
unifiable”; otherwise, if
t' = f(t'1,…, t'k), t'' = f (t''1,…, t''k),
replace the equation with k new equations
t'1 = t''1,…, t'k = t''k
(4) If x = t is an equation such that x appears elsewhere in the system:
– if x appears in t, output “not unifiable”
– if x appears in other equations, replace all occurrences of x in those
equation with t
www.sti-innsbruck.at
72
Unification Algorithm – Example
•
•
•
•
•
•
•
•
Consider the system of term equations:
g(y) = x, f(x, h(x), y) = f(g(z),w, z)
Start by using Rule 3 to replace the second equation with three equations:
g(y) = x, x = g(z), h(x) = w, y = z
Next, use Rule 1 to rewrite the first and the third equation:
x = g(y), x = g(z), w = h(x), y = z
Using the first equation, eliminate x from the right-hand sides of the
remaining equations:
x = g(y), g(y) = g(z), w = h(g(y)), y = z
Next, using Rule 3, rewrite the second equation:
x = g(y), y = z, w = h(g(y)), y = z
The last equation is redundant (it is identical to the second equation) and
we can delete it:
x = g(y), y = z, w = h(g(y))
Finally, use the second equation to eliminate y from the right-hand sides of
other equations:
x = g(z), y = z, w = h(g(z))
This system is in solved form, so m.g.u is:
μ = {x ← g(z), y ← z,w ← h(g(z))}
www.sti-innsbruck.at
73
General Resolution
• Suppose L = {l1, l2,…, lm} is a set of literals. Then, we
define its complement as Lc = {lc1, lc2,…, lcm}
• General Resolution Rule: Suppose C1 and C2 are two
clauses with no variables in common. Let
so that L1 and Lc2 can be unified using an m.g.u. σ.
Then, C1 and C2 are said to be clashing clauses and
their resolvent is
Res(C1, C2) = (C1σ − L1σ) U (C2σ − L2σ)
www.sti-innsbruck.at
74
General Resolution (cont’)
• Example: Consider the two clauses
C1 = p(f(x), g(y)) \/ q(x, y)
C2 = ¬p(f(f(a), g(z)) \/ q(f(a), g(z))
These two clauses contain the following literals:
L1 = {p(f(x), g(y))}
L2 = {¬p(f(f (a), g(z))}
so that Lc2 = {p(f(f(a)), g(z))}.
It is easy to check that the literals in L1 and Lc2 are unifiable with an
m.g.u.
σ = {x ← f (a), y ← z}
so the clauses C1 and C2 are clashing, and their resolvent is:
Res(C1, C2) = (C1σ − L1σ) U (C2σ − L2σ)
= {q(f(a), z)} U {q(f(a), g(z))}
so that we get the clause q(f(a), z) \/ q(f(a), g(z))
www.sti-innsbruck.at
75
General Resolution (cont’)
•
•
•
Most often, the two clauses we are trying to resolve will have variables in
common, so we cannot use the Resolution Rule as stated before
Before we attempt to resolve such pairs of clauses, we have to standardize
apart; i.e. we have to rename the variables so that the clauses no longer
have any variables in common
Example: Consider the two literals
p(f(x), y), ¬p(x, a)
The two atoms contain the same variable x, so we have to standardize them
apart before attempting to resolve; e.g. we can replace x in the second atom
with z:
p(f(x), y), ¬p(z, a)
It is easy to see that an m.g.u. is σ = {z ← f (x), y ← a}. The m.g.u.
transforms the pair of literals into:
p(f(x), a), ¬p(f (x), a)
Now, we can apply resolution to this pair of literals to obtain the empty
clause.
www.sti-innsbruck.at
76
General Resolution Procedure
• Input: A set of clauses S
• Output: “satisfiable” or “not satisfiable”, in the case the algorithm
terminates
• Set S0 := S
• Suppose Si has been constructed
• Choose a pair of clashing clauses C1, C2 in Si and find
C = Res(C1, C2)
(we may need to standardize apart certain clauses during this step)
• If C = □ (i.e. empty clause), terminate the procedure and output “not
• satisfiable”; otherwise, put
Si+1 := Si U {C}
• • If Si+1 = Si, for all possible pairs of clashing clauses in Si, terminate
the procedure and output “satisfiable”
www.sti-innsbruck.at
77
General Resolution Procedure – Example
• Example: Show, using the general resolution procedure, that
the set of clauses 1-7 is unsatisfiable.
This is shown in lines 8-15 which are a refutation by the
resolution procedure (each line contains the resolvent, the
mgu and the number of the parent classes)
www.sti-innsbruck.at
78
General Resolution Procedure – Soundness and
Completeness
• Theorem (Soundness of Resolution) If the empty
clause is derived by general resolution, then S
is unsatisfiable.
• Theorem (Completeness of Resolution) If a set
of clauses S is unsatisfiable, then the empty
clause can be derived from S using general
resolution.
www.sti-innsbruck.at
79
ILLUSTRATION BY LARGER
EXAMPLES
www.sti-innsbruck.at
80
Example 1
• Show that
is not valid using the semantic tableaux method
Solution: It suffices to show that the negation of the
formula
is satisfiable. In fact, we will also find the smallest model
for this negation, i.e. the smallest structure in which the
original formula fails to be true.
– From
descendent
, we get the
– As the next level of the tableau, we get:
– After introducing two new constant symbols a and b:
www.sti-innsbruck.at
81
Example 1 (cont’)
– We can now generate the following instances of the universal
formula:
– After this, it can be shown that, after branching off different
possibilities for p(a) \/ q(a) and p(b) \/ q(b), we will never be able
to terminate all the branches and mark them as closed.
• In fact, by examining what happens after the tree starts
branching, one can show by following one of the
branches that the smallest model for the negation has
the universe {a, b} and that the relations are defined as
follows:
p(a), ¬q(a), ¬p(b), q(b)
which will falsify the original formula.
www.sti-innsbruck.at
82
Example 2
• Prove, in the Hilbert proof system for predicate logic, that
Solution:
www.sti-innsbruck.at
83
Example 2
• Transform each of the following formulas to the
clausal form:
Solution:
www.sti-innsbruck.at
84
Example 2 (cont’)
www.sti-innsbruck.at
85
Example 3
• Prove the validity of
by resolution refutation of its negation.
Solution:
First, consider the negation of the formula:
Convert the above formula into a PCNF:
www.sti-innsbruck.at
86
Example 3 (cont’)
Finally, try to refute the set of clauses
{¬A(x) \/ B(x),A(f(x)),¬B(z)}
First, unify ¬A(x) \/ B(x) and A(f(y)) using
{x ← f(y)}
to get as the resolvent
B(f(y))
Next, unify B(f(y)) and B(z) using the unifier
{z ← f(y)}
and apply resolution to get the empty clause. So,
is unsatisfiable, which means that its complement is a
valid formula of predicate logic
www.sti-innsbruck.at
87
Example 4
• Find out if the formula
is a logical consequence of the set of formulas
Solution: We use resolution to determine whether
is a logical consequence of the formulas
Note that C is a logical consequence of A and B iff the formula A /\ B
→ C is valid. This, in turn, is equivalent to checking whether ¬(A /\ B
→ C) A /\ B /\ ¬C is unsatisfiable.
www.sti-innsbruck.at
88
Example 4 (cont’)
Skolemize A, B, and ¬C to get the following set of universal
formulas:
where f, g, h, i are new unary function symbols, and a, b are new
constant symbols
So, we need to check if the following set of clauses is unsatisfiable:
Each clause in S contains a negative literal. In general, if both
premises of a resolution rule contain a negative literal, so does the
conclusion. Thus, we can only derive clauses with negative literals
from S (by resolution), but not the empty clause (a contradiction).
Therefore, S is satisfiable and C cannot be a logical consequence of
A and B.
www.sti-innsbruck.at
89
EXTENSIONS
www.sti-innsbruck.at
90
Extensions
• The characteristic feature of first-order logic is that individuals can
be quantified, but not predicates; second-order logic extends firstorder logic by adding the latter type of quantification
• Other higher-order logics allow quantification over even higher types
than second-order logic permits
– These higher types include relations between relations, functions from
relations to relations between relations, and other higher-type objects
• Ordinary first-order interpretations have a single domain of
discourse over which all quantifiers range; many-sorted first-order
logic allows variables to have different sorts, which have different
domains
www.sti-innsbruck.at
91
Extensions (cont’)
• Intuitionistic first-order logic uses intuitionistic rather than classical
propositional calculus; for example, ¬¬φ need not be equivalent to
φ; similarly, first-order fuzzy logics are first-order extensions of
propositional fuzzy logics rather than classical logic
• Infinitary logic allows infinitely long sentences; for example, one may
allow a conjunction or disjunction of infinitely many formulas, or
quantification over infinitely many variables
• First-order modal logic has extra modal operators with meanings
which can be characterised informally as, for example "it is
necessary that φ" and "it is possible that φ“
www.sti-innsbruck.at
92
SUMMARY
www.sti-innsbruck.at
93
Summary
• Predicate logic differentiates from propositional logic by
its use of quantifiers
– Each interpretation of predicate logic includes a domain of
discourse over which the quantifiers range.
• There are many deductive systems for predicate logic
that are sound (only deriving correct results) and
complete (able to derive any logically valid implication)
• The logical consequence relation in predicate logic is
only semidecidable
• This lecture focused on three core aspects of the
propositional logic: Syntax, Semantics, and Reasoning
www.sti-innsbruck.at
94
REFERENCES
www.sti-innsbruck.at
95
References
• Mathematical Logic for Computer Science (2nd edition)
by Mordechai Ben-Ari
– http://www.springer.com/computer/foundations/book/978-185233-319-5
• Propositional Logic at Stanford Encyclopedia of
Philosophy
– http://plato.stanford.edu/entries/logic-classical/
• First-order logic on Wikipedia
– http://en.wikipedia.org/wiki/First-order_logic
• Many online resources
– http://www.google.com/search?q=predicate+logic
– http://www.google.com/search?hl=en&q=First-order+logic
www.sti-innsbruck.at
96
Next Lecture
#
Date
Title
1
Introduction
2
Propositional Logic
3
Predicate Logic
4
Theorem Proving, Logic Programming, and Description Logics
5
Search methods
6
CommonKADS
7
Problem-Solving Methods
8
Planning
9
Agents
10
Rule learning
11
Inductive Logic Programming
12
Formal Concept Analysis
13
Neural Networks
14
Semantic Web and Exam Preparation
www.sti-innsbruck.at
97
Questions?
www.sti-innsbruck.at
98