Transcript Logic - University College Cork

Course:
Engineering Artificial Intelligence
Dr. Radu Marinescu
Lecture 7
University College Cork (Ireland) Department of Civil and Environmental Engineering
Today’s class
o
Logic
• Propositional logic
• First order logic
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 2
What is logic?
o
A formal language
• Syntax – what expressions are legal
• Semantics – what legal expressions mean
• Proof system – a way of manipulating syntactic expressions to get
other syntactic expressions (which will tell us something new)
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 3
What is logic?
o
A formal language
• Syntax – what expressions are legal
• Semantics – what legal expressions mean
• Proof system – a way of manipulating syntactic expressions to get
other syntactic expressions (which will tell us something new)
o
Why proofs? Two kinds of inferences an agent
might want to make
• Multiple percepts => conclusions about the world
• Current state & operators => properties of next state
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 4
Propositional logic syntax
o
Syntax: what you’re allowed to write
•for (int t = 0; t == 100; t++) {…}
• “Colorless green ideas sleep furiously” (Noam Chomsky)
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 5
Propositional logic syntax
o
Syntax: what you’re allowed to write
•for (int t = 0; t == 100; t++) {…}
• “Colorless green ideas sleep furiously” (Noam Chomsky)
o
Sentences (WFF: well formed formulas)
•true and false are sentences
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 6
Propositional logic syntax
o
Syntax: what you’re allowed to write
•for (int t = 0; t == 100; t++) {…}
• “Colorless green ideas sleep furiously” (Noam Chomsky)
o
Sentences (WFF: well formed formulas)
•true and false are sentences
• Propositional variables are sentences: P, Q, R, Z
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 7
Propositional logic syntax
o
Syntax: what you’re allowed to write
•for (int t = 0; t == 100; t++) {…}
• “Colorless green ideas sleep furiously” (Noam Chomsky)
o
Sentences (WFF: well formed formulas)
•true and false are sentences
• Propositional variables are sentences: P, Q, R, Z
• If Φ and Ψ are sentences, then so are
(Φ), ¬ Φ, Φ /\ Ψ, Φ \/ Ψ, Φ → Ψ, Φ ↔ Ψ
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 8
Propositional logic syntax
o
Syntax: what you’re allowed to write
•for (int t = 0; t == 100; t++) {…}
• “Colorless green ideas sleep furiously” (Noam Chomsky)
o
Sentences (WFF: well formed formulas)
•true and false are sentences
• Propositional variables are sentences: P, Q, R, Z
• If Φ and Ψ are sentences, then so are
(Φ), ¬ Φ, Φ ˄ Ψ, Φ ˅ Ψ, Φ → Ψ, Φ ↔ Ψ
• Nothing else is a sentence
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 9
Precedence
¬
˄
A˅B˄C
A ˅ (B ˄ C)
˅
A˄B→C˅D
(A ˄ B) → (C ˅ D)
→
A→B˅C↔D
(A → (B ˅ C)) ↔ D
↔
o
o
highest
lowest
Precedence rules enable “shorthand” form of sentences, but
formally only the fully parenthesized form is legal
Syntactically ambiguous forms allowed in shorthand only when
semantically equivalent: A ˄ B ˄ C is equivalent to (A ˄ B) ˄ C
and A ˄ (B ˄ C)
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 10
Semantics
o
o
Meaning of a sentence is truth value {t, f}
Interpretation is an assignment of truth values to
propositional variables
• holds(Φ, i) [Sentence Φ is t in interpretation i]
• fails(Φ, i)
[Sentence Φ is f in interpretation i]
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 11
Semantic rules
holds(true, i) for all i
o fails(false, i) for all I
o holds(¬Φ, i)
if and only if fails(Φ, i)
o
(negation)
o
holds(Φ ˄ Ψ, i) iff holds(Φ, i) and holds(Ψ, i)
(conjunction)
o
holds(Φ ˅ Ψ, i) iff holds(Φ, i) or holds(Ψ, i)
(disjunction)
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 12
Semantic rules
holds(true, i) for all i
o fails(false, i) for all I
o holds(¬Φ, i)
if and only if fails(Φ, i)
o
(negation)
o
holds(Φ ˄ Ψ, i) iff holds(Φ, i) and holds(Ψ, i)
(conjunction)
o
holds(Φ ˅ Ψ, i) iff holds(Φ, i) or holds(Ψ, i)
(disjunction)
o
o
holds(P, i) iff i(P) = t
fails(P, i) iff i(P) = f
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 13
Some important shorthand
o
Φ → Ψ ≡ ¬Φ ˅ Ψ (conditional, implication)
antecedent → consequent
o
Φ ↔ Ψ ≡ (Φ → Ψ) ˄ (Ψ → Φ) (biconditional,
equivalence)
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 14
Some important shorthand
o
Φ → Ψ ≡ ¬Φ ˅ Ψ (conditional, implication)
antecedent → consequent
o
Φ ↔ Ψ ≡ (Φ → Ψ) ˄ (Ψ → Φ) (biconditional,
equivalence)
Truth tables
P
Q
¬P
P˄Q
P˅Q
P→Q Q→P P↔Q
f
f
t
f
f
t
t
t
f
t
t
f
t
t
f
f
t
f
f
f
t
f
t
f
t
t
f
t
t
t
t
t
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 15
Some important shorthand
o
Φ → Ψ ≡ ¬Φ ˅ Ψ (conditional, implication)
antecedent → consequent
o
Φ ↔ Ψ ≡ (Φ → Ψ) ˄ (Ψ → Φ) (biconditional,
equivalence)
Truth tables
P
Q
¬P
P˄Q
P˅Q
P→Q Q→P P↔Q
f
f
t
f
f
t
t
t
f
t
t
f
t
t
f
f
t
f
f
f
t
f
t
f
t
t
f
t
t
t
t
t
Note that implication is not “causality”, if P is f then P→Q is t
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 16
Terminology
o
A sentence is valid iff its truth table value is t in
all interpretations
• Valid sentences: true, ¬false, P ˅ ¬P
o
A sentence is satisfiable iff its truth value is t in
at least one interpretation
• Valid sentences: P, true, ¬P
o
A sentence is unsatisfiable iff its truth value is f
in all interpretations
• Unsatisfiable sentences: P ˄¬P, false, ¬true
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 17
Terminology
o
A sentence is valid iff its truth table value is t in
all interpretations
• Valid sentences: true, ¬false, P ˅ ¬P
o
A sentence is satisfiable iff its truth value is t in
at least one interpretation
• Valid sentences: P, true, ¬P
o
A sentence is unsatisfiable iff its truth value is f
in all interpretations
• Unsatisfiable sentences: P ˄¬P, false, ¬true
All are finitely decidable!
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 18
Examples
Sentence
Valid?
smoke → fire
smoke ˅ ¬fire
valid
Interpretation that make
sentence’s truth value = f
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 19
Examples
Sentence
Valid?
smoke → smoke
¬ smoke ˅ smoke
valid
smoke → fire
¬ smoke ˅ fire
satisfiable,
not valid
Interpretation that make
sentence’s truth value = f
smoke = t, fire = f
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 20
Examples
Sentence
Valid?
smoke → smoke
¬smoke ˅ smoke
valid
Interpretation that make
sentence’s truth value = f
smoke → fire
¬smoke ˅ fire
satisfiable,
not valid
smoke = t, fire = f
(s → f) → (¬s → ¬f)
satisfiable,
not valid
s = f, f = t
s → f = t, ¬s → ¬f = f
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 21
Examples
Sentence
Valid?
smoke → smoke
¬smoke ˅ smoke
valid
Interpretation that make
sentence’s truth value = f
smoke → fire
¬smoke ˅ fire
satisfiable,
not valid
smoke = t, fire = f
(s → f) → (¬s → ¬f)
satisfiable,
not valid
s = f, f = t
s → f = t, ¬s → ¬f = f
(s → f) → (¬f → ¬s)
valid
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 22
Satisfiability
o
o
o
Related to constraint satisfaction
Given a sentence S, try to find an interpretation i
such that holds(S, i)
Analogous to finding an assignment of values to
variables such that the constraints hold
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 23
Satisfiability
o
o
Related to constraint satisfaction
Given a sentence S, try to find an interpretation i
such that holds(S, i)
o
Analogous to finding an assignment of values to
variables such that the constraints hold
o
Brute force method: enumerate all
interpretations and check
Better methods
o
• Heuristic search
• Constraint propagation
• Stochastic search
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 24
Satisfiability problems
o
Scheduling nurses to work in a hospital
• Propositional variables represent, for example, that Pat is working
on Tuesday at 2
• Constraints on the schedule are represented using logical
expressions over the variables
o
Finding bugs in software
• Propositional variables represent states of the program
• Use logic to describe how the program works and to assert there
is a bug
• If the sentence is satisfiable, you’ve found a bug
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 25
A good lecture?
o
Imagine we knew that:
• If today is sunny, then Thomas will be happy (S → H)
• If Thomas is happy, the lecture will be good (H → G)
• Today is sunny (S)
Should we conclude that the lecture will be good?
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 26
Checking interpretations
S
H
G
t
t
t
t
t
f
t
f
t
t
f
f
f
t
t
f
t
f
f
f
t
f
f
f
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 27
Checking interpretations
S
H
G
S→H
H→G
S
t
t
t
t
t
t
t
t
f
t
f
t
t
f
t
f
t
t
t
f
f
f
t
t
f
t
t
t
t
f
f
t
f
t
f
f
f
f
t
t
t
f
f
f
f
t
t
f
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 28
Checking interpretations
S
H
G
S→H
H→G
S
G
t
t
t
t
t
t
t
t
t
f
t
f
t
f
t
f
t
f
t
t
t
t
f
f
f
t
t
f
f
t
t
t
t
f
t
f
t
f
t
f
f
f
f
f
t
t
t
f
t
f
f
f
t
t
f
f
Good
lecture!
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 29
Entailment
o
A knowledge base (KB) entails a sentence S iff
every interpretation that makes KB true also
makes S true
KB
holds
holds
holds
interpretations
S
subset
interpretations
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 30
Computing entailment
Enumerate all interpretations
o Select those in which all elements of KB are true
o Check to see if S is true in all those
interpretations
o
KB
holds
holds
holds
interpretations
S
subset
interpretations
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 31
Computing entailment
Enumerate all interpretations
o Select those in which all elements of KB are true
o Check to see if S is true in all those
interpretations
o
Way too many interpretations in general !!
KB
holds
holds
holds
interpretations
S
subset
interpretations
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 32
Entailment and Proof
o
A proof is a way to test whether a KB entails a
sentence, without enumerating all possible
interpretations
proof
KB
holds
holds
holds
interpretations
S
subset
interpretations
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 33
Proof
Proof is a sequence of sentences
o First ones are premises (in KB)
o Then, you can write down on the next line the result
of applying an inference rule to previous lines
o When S is on a line, you have proved S from KB
o
o
o
If inference rules are sound, then any S you can
prove from KB is entailed by KB
If inference rules are complete, then any S that is
entailed by KB can be proved from KB
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 34
Natural deduction
o
Some inference rules
α→β
α→β
α
α
¬β
β
α˄β
β
¬α
α˄β
α
Modus
ponens
Modus
tolens
ANDintroduction
ANDelimination
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 35
Natural deduction example
Prove S
Step
Formula
Derivation
1
P˄Q
given
2
P→R
given
3
(Q ˄ R) → S
given
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 36
Natural deduction example
Prove S
Step
Formula
Derivation
1
P˄Q
given
2
P→R
given
3
(Q ˄ R) → S
given
4
P
1 And-Elim
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 37
Natural deduction example
Prove S
Step
Formula
Derivation
1
P˄Q
given
2
P→R
given
3
(Q ˄ R) → S
given
4
P
1 And-Elim
5
R
4,2 Modus Ponens
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 38
Natural deduction example
Prove S
Step
Formula
Derivation
1
P˄Q
given
2
P→R
given
3
(Q ˄ R) → S
given
4
P
1 And-Elim
5
R
4,2 Modus Ponens
6
Q
1 And-Elim
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 39
Natural deduction example
Prove S
Step
Formula
Derivation
1
P˄Q
given
2
P→R
given
3
(Q ˄ R) → S
given
4
P
1 And-Elim
5
R
4,2 Modus Ponens
6
Q
1 And-Elim
7
Q˄R
5,6 And-Intro
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 40
Natural deduction example
Prove S
Step
Formula
Derivation
1
P˄Q
given
2
P→R
given
3
(Q ˄ R) → S
given
4
P
1 And-Elim
5
R
4,2 Modus Ponens
6
Q
1 And-Elim
7
Q˄R
5,6 And-Intro
8
S
7,3 Modus Ponens
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 41
Proof systems
o
There are many natural deduction systems; they
are typically “proof checkers”, sound but not
complete
o
Natural deduction uses lots of inference rules
which introduces a large branching factor in the
search for a proof
o
In general, you need to do “proof by cases”
which introduces even more branching
Prove R
1
P˅R
2
Q˅R
3
P→R
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 42
Propositional resolution
o
Resolution rule:
α˅β
¬β ˅ γ
α˅γ
o
Single inference rule is a sound and complete
proof system
o
Requires all sentences to be converted to
conjunctive normal form (CNF)
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 43
Conjunctive normal form (CNF)
o
Conjunctive normal form (CNF) formulas:
A  B  C   B  D  A  B  C 
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 44
Conjunctive normal form (CNF)
o
Conjunctive normal form (CNF) formulas:
A  B  C   B  D  A  B  C 
• (A ˅ B ˅ ¬C) is a clause, which is a disjunction of
literals
• A, B, and ¬C are literals, each of which is a variable
or the negation of a variable
• Each clause is a requirement that must be satisfied
and can be satisfied in multiple ways
• Every sentence in propositional logic can be written in
CNF
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 45
Converting to CNF
1.
2.
Eliminate arrows using definitions
Drive in negations using De Morgan’s Laws
       
      
3.
Distribute OR over AND
A  B  C    A  B   A  C 
4.
Every sentence can be converted to CNF, but it
may grow exponentially in size
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 46
CNF conversion example
A  B  C  D
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 47
CNF conversion example
A  B  C  D
1.
Eliminate arrows
 A  B  C  D
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 48
CNF conversion example
A  B  C  D
1.
Eliminate arrows
 A  B  C  D
2.
Drive in negations
A  B  C  D
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 49
CNF conversion example
A  B  C  D
1.
Eliminate arrows
 A  B  C  D
2.
Drive in negations
3.
Distribute
A  B  C  D
A  C  D  B  C  D
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 50
Propositional resolution
o
Resolution rule:
α˅β
¬β ˅ γ
α˅γ
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 51
Propositional resolution
o
Resolution rule:
α˅β
¬β ˅ γ
α˅γ
o
Resolution refutation:
• Convert all sentences to CNF
• Negate the desired conclusion (converted to CNF)
• Apply resolution until either
 Derive false (a contradiction)
 Can’t apply any more
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 52
Propositional resolution
o
Resolution refutation:
• Convert all sentences to CNF
• Negate the desired conclusion (converted to CNF)
• Apply resolution until either
 Derive false (a contradiction)
 Can’t apply any more
o
Resolution refutation is sound and complete
• If we derive a contradiction, then the conclusion follows from
axioms
• If we can’t apply any more, then the conclusion cannot be proved
from the axioms
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 53
Propositional resolution example
Prove R
1
P˅Q
2
P→R
3
Q→R
Step
Formula
Derivation
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 54
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 55
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 56
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 57
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
4
¬R
negated conclusion
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 58
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
4
¬R
negated conclusion
5
Q˅R
1,2
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 59
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
4
¬R
negated conclusion
5
Q˅R
1,2
6
¬P
2,4
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 60
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
4
¬R
negated conclusion
5
Q˅R
1,2
6
¬P
2,4
7
¬Q
3,4
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 61
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
4
¬R
negated conclusion
5
Q˅R
1,2
6
¬P
2,4
7
¬Q
3,4
8
R
5,7
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 62
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
4
¬R
negated conclusion
5
Q˅R
1,2
6
¬P
2,4
7
¬Q
3,4
8
R
5,7
9
[]
4,8
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 63
Propositional resolution example
Prove R
Step
Formula
Derivation
1
P˅Q
1
P˅Q
given
2
P→R
2
¬P ˅ R
given
3
Q→R
3
¬Q ˅ R
given
4
¬R
negated conclusion
5
Q˅R
1,2
6
¬P
2,4
7
¬Q
3,4
false ˅ R
8
R
5,7
¬R ˅ false
9
[]
4,8
false ˅ false
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 64
Example problem
Prove R
1
(P → Q) → Q
2
(P → R) → R
3
(R →S) → ¬(S → Q)
Do it yourselves!
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 65
Proof strategies
o
Unit preference: prefer a resolution step involving a
unit clause (clause with one literal)
• Produces a shorter clause – which is good since we are trying to
produce a zero-length clause, that is a contradiction
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 66
Proof strategies
o
Unit preference: prefer a resolution step involving a
unit clause (clause with one literal)
• Produces a shorter clause – which is good since we are trying to
produce a zero-length clause, that is a contradiction
o
Set of support: choose a resolution involving the
negated goal or any clause derived from the
negated goal
• We’re trying to produce a contradiction that follows from the
negated goal, so these are “relevant” clauses
• If a contradiction exists, one can find one using the set-of-support
strategy
University College Cork (Ireland) Department of Civil and Environmental Engineering
R. Marinescu October-2009
page 67