Representation and Interaction
Chantal Drijvers
March 2021
Logic and Resolution
Logic concepts
• M |=ϕ
– M satisfies ϕ
– If a formula ϕ is true under a given interpretation M
• A formula is satisfiable if there is some interpretation under which it is
true
• A formula is unsatisfiable (inconsistent) if there is no interpretation under
which it is true
• |=ϕ
– Formula is valid (tautology)
– If a formula is true in every interpretation
– for all M: M |=ϕ
• Γ |=ϕ
– Formula ϕ is entailed (logical consequence) by a conjunction of for-
mulas (theory) Γ, if for all M: M |=Γ then M |=ϕ
• w |=ϕ
– w is a model of ϕ
1
,Deduction Concepts
• Deductive system S: set of axioms and rules of inference for deriving the-
orems
• A formula ϕ can be deduced by a set of formulae Γ if ϕ can be proven
using a deduction system S, written as Γ ` sϕ
• A deductive system S is sound if
Γ ` sϕ ⇒ Γ |= ϕ
• A deductive system S is complete if
Γ |= ϕ ⇒ Γ ` sϕ
• A deductive system S is refutation-complete if
Γ |= ⇒ Γ ` s
2
,Resolution
• Clausal form
L1 ∨ L2 ∨ · · · ∨ Ln
– Li : literal (atom or negation of atom)
– if n = 0, then it is (empty clause)
• Complementary literals: L an L’, such that L ≡ ¬ L’
• Resolution (rule) R
C ∨ L, C 0 ∨ ¬L
D
– C, C’: clause
– D: (binary) resolvent equal to C ∨ C’
• V = {P ∨ Q ∨ ¬R, U ∨ ¬Q}, then
P ∨ Q ∨ ¬R, U ∨ ¬Q
P ∨ U ∨ ¬R
So V `R P ∨ U ∨ ¬R by applying the resolution rule R once
¬P ∨Q,¬Q ¬P ,P
• Give V = {¬P ∨ Q, ¬Q, P }, then ¬P and so V `R
• V `R
– V is inconsistent
– The derivation is called a refutation
– R is sound
• V 0R
– V is consistent
– R is refutation-complete
• Horn clause: clause with maximally one positive literal ¬A1 ∨· · ·∨¬Am ∨
B, also denoted by B ← A1 , . . . , Am
3
, First-order Logic
Syntax
• Constants: a, b, ...
• Variables: x, y, z, ...
• Functions: maps (sets of) objects to other objects, e.g., father, plus, ...
• Predicates: a function that returns either true of false: Brother-of, Bigger-
than, Has-color, ...
• Quantifiers: allow the representation of properties that hold for a collec-
tion to objects
– Existential: ∃x, ’there is an x’
– Universal: ∀x, ’for all x’
Truth
• A predicate is true if the interpretation of the predicate evaluates to ’true’
• Logical connectives are interpreted just like in propositional logic
• ∀xϕ(x) is true if ϕ is true for all variable assignments
• ∃xϕ(x) is true if ϕ is true for some variable assignments
Equivalences
¬(¬F ) ≡ F (a)
F ∨G ≡ G∨F (b)
F ∧G ≡ G∧F (c)
(F ∧ G) ∧ H ≡ F ∧ (G ∧ H) (d)
(F ∨ G) ∨ H ≡ F ∨ (G ∨ H) (e)
F ∨ (G ∧ H) ≡ (F ∨ G) ∧ (F ∨ H) (f)
F ∧ (G ∨ H) ≡ (F ∧ G) ∨ (F ∧ H) (g)
F ↔G ≡ (F → G) ∧ (G → F ) (h)
F →G ≡ ¬F ∨ G (i)
¬(F ∧ G) ≡ ¬F ∨ ¬G (j)
¬(F ∨ G) ≡ ¬ ∧ ¬G (k)
F ∧F ≡ F (l)
F ∨F ≡ F (m)
Table 1: Equivalences
4
Chantal Drijvers
March 2021
Logic and Resolution
Logic concepts
• M |=ϕ
– M satisfies ϕ
– If a formula ϕ is true under a given interpretation M
• A formula is satisfiable if there is some interpretation under which it is
true
• A formula is unsatisfiable (inconsistent) if there is no interpretation under
which it is true
• |=ϕ
– Formula is valid (tautology)
– If a formula is true in every interpretation
– for all M: M |=ϕ
• Γ |=ϕ
– Formula ϕ is entailed (logical consequence) by a conjunction of for-
mulas (theory) Γ, if for all M: M |=Γ then M |=ϕ
• w |=ϕ
– w is a model of ϕ
1
,Deduction Concepts
• Deductive system S: set of axioms and rules of inference for deriving the-
orems
• A formula ϕ can be deduced by a set of formulae Γ if ϕ can be proven
using a deduction system S, written as Γ ` sϕ
• A deductive system S is sound if
Γ ` sϕ ⇒ Γ |= ϕ
• A deductive system S is complete if
Γ |= ϕ ⇒ Γ ` sϕ
• A deductive system S is refutation-complete if
Γ |= ⇒ Γ ` s
2
,Resolution
• Clausal form
L1 ∨ L2 ∨ · · · ∨ Ln
– Li : literal (atom or negation of atom)
– if n = 0, then it is (empty clause)
• Complementary literals: L an L’, such that L ≡ ¬ L’
• Resolution (rule) R
C ∨ L, C 0 ∨ ¬L
D
– C, C’: clause
– D: (binary) resolvent equal to C ∨ C’
• V = {P ∨ Q ∨ ¬R, U ∨ ¬Q}, then
P ∨ Q ∨ ¬R, U ∨ ¬Q
P ∨ U ∨ ¬R
So V `R P ∨ U ∨ ¬R by applying the resolution rule R once
¬P ∨Q,¬Q ¬P ,P
• Give V = {¬P ∨ Q, ¬Q, P }, then ¬P and so V `R
• V `R
– V is inconsistent
– The derivation is called a refutation
– R is sound
• V 0R
– V is consistent
– R is refutation-complete
• Horn clause: clause with maximally one positive literal ¬A1 ∨· · ·∨¬Am ∨
B, also denoted by B ← A1 , . . . , Am
3
, First-order Logic
Syntax
• Constants: a, b, ...
• Variables: x, y, z, ...
• Functions: maps (sets of) objects to other objects, e.g., father, plus, ...
• Predicates: a function that returns either true of false: Brother-of, Bigger-
than, Has-color, ...
• Quantifiers: allow the representation of properties that hold for a collec-
tion to objects
– Existential: ∃x, ’there is an x’
– Universal: ∀x, ’for all x’
Truth
• A predicate is true if the interpretation of the predicate evaluates to ’true’
• Logical connectives are interpreted just like in propositional logic
• ∀xϕ(x) is true if ϕ is true for all variable assignments
• ∃xϕ(x) is true if ϕ is true for some variable assignments
Equivalences
¬(¬F ) ≡ F (a)
F ∨G ≡ G∨F (b)
F ∧G ≡ G∧F (c)
(F ∧ G) ∧ H ≡ F ∧ (G ∧ H) (d)
(F ∨ G) ∨ H ≡ F ∨ (G ∨ H) (e)
F ∨ (G ∧ H) ≡ (F ∨ G) ∧ (F ∨ H) (f)
F ∧ (G ∨ H) ≡ (F ∧ G) ∨ (F ∧ H) (g)
F ↔G ≡ (F → G) ∧ (G → F ) (h)
F →G ≡ ¬F ∨ G (i)
¬(F ∧ G) ≡ ¬F ∨ ¬G (j)
¬(F ∨ G) ≡ ¬ ∧ ¬G (k)
F ∧F ≡ F (l)
F ∨F ≡ F (m)
Table 1: Equivalences
4
