Proof

Question 1

Meaning of A ⊨ B

Answer 1

A ⊨ B means that B is true in every structure in which A is true.

Question 2

Meaning of A ⊢ B

Answer 2

A ⊢ B means B can be proved using A as the premises.

Question 3

Soundness

Answer 3

If A ⊢ B then A ⊨ B

Question 4

Completeness

Answer 4

If A ⊨ B then A ⊢ B

Question 5

reductio ad absurdum

Answer 5

An assumption is rejected because it leads to a contradiction (an absurdity).

Question 6

AND introduction

Answer 6

Question 7

AND elimination

Answer 7

Question 8

OR Introduction

Answer 8

Question 9

OR Elimination

Answer 9

Question 10

NOT Introduction

Answer 10

Question 11

NOT Elimination

Answer 11

Question 12

IMPLIES Introduction

Answer 12

Question 13

IMPLIES Elimination

Answer 13

Question 14

Double negation elimination

Answer 14

Question 15

Excluded middle

Answer 15

⊢ A ∨ ¬A

Question 16

Universal Elimination

Answer 16

• We know that for all x the statement p holds.
• We have a term t that we need to use in our argument.
• So we know that the statement p holds if we replace x by t everywhere in the statement.

Question 17

Universal introduction

Answer 17

• We are using x for a completely arbitrary element of the domain, being careful not to assume it has any special properties.
• We show that x has to have the property stated in the formula p.
• Because x was arbitrary, we conclude that the formula p must hold for all x.

Question 18

Existential elimination

Answer 18

• We know there is some x with the property stated by p.
• Let’s introduce a new name, a, for a particular thing with this property.
• We deduce that some statement, s, (not involving a) must hold by an argument using the assumption that a has propertyp.
• We conclude that s holds on its own, without the assumption about a having property p.

Question 19

Existential introduction

Answer 19

• We have a statement p about some particular term t.
• We conclude that there is some x with the property stated by p where we replace t by x.

Question 20

literal

Answer 20

A WFF which is either an atom (an atomic proposition) or the negation of an atom.

Question 21

Clause

Answer 21

A set of literals.

A clause is used to stand for the disjunction of its elements.
[a, ¬b] refers to both:
- a ∨ ¬b
- ¬b ∨ a

Question 22

Horn clauses

Answer 22

Clauses with at most one positive literal.

Question 23

Equivalent clause to false

Answer 23

Empty clause
[]

Question 24

Equivalent disjunction to a → b

Answer 24

¬a ∨ b

Question 25

Clausal resolution

Answer 25

α is an atom
Σ₁ and Σ₂ are clauses

α is called the atom resolved upon.
Σ₁ and Σ₂ is the resolvent.

Question 26

Procedure for reduction to CNF

Answer 26

1. Replace any → by using ¬ A ∨ B instead of A → B
   2.
   - Replace any wff of form ¬¬A by A
   - Replace ¬ ( A ∨ B ) by ¬A ∧ ¬B
   - Replace ¬ ( A ∧ B ) by ¬A ∨ ¬B
   3.
   - Replace A ∨ ( B ∧ C ) by (A ∨ B) ∧ ((A ∨ C)
   - Replace (A ∧ B) ∨ C by (A ∨ C) ∧ ( B ∨ C )

Question 27

Clausal Form

Answer 27

We write
( a ∨ b ) ∧ ( c ∨ d ) ∧ ( a ∨ d ∨ e )
in the form
{ [a, b], [c, d], [a, d, e] }

The innermost sets are treated as disjunctions of their elements, the whole is treated as the conjunction of its elements.

Question 28

Equivalent clause to true

Answer 28

Empty conjunction
{ }

Question 29

Resolution Refutation Procedure

Answer 29

Given a finite set of wffs Δ and a wff f, carry out this procedure:

1. Convert Δ to CNF, giving a set of clauses, Φ.
2. Convert the negation of f to CNF giving Ψ.
3. Let Γ = Φ ∨ Ψ
4. Iteratively apply resolution to the clauses in Γ adding the resolvents to Γ.

Continue until no more resolution is possible or until the empty clause is a resolvent.

Question 30

Resolution in first-order logic

Answer 30

• Convert knowledge base and negated query to clauses
• Keep resolving until get empty clause or cannot continue

Question 31

Convert to clausal form: first order case
6 Steps

Answer 31

1. Eliminate →
2. Move ¬ inwards
   - ¬∀x ɑ rewrites to ∃x ¬ɑ
   - ¬∃x ɑ rewrites to ∀x ¬ɑ
3. Eliminate remaining variables (Skolemization)
4. Rename variables so v different for each ∀v.
5. Move ∀s to the front
6. Distribute ∧ over ∨

Finally, rename variables so different clauses have different variables.

Question 32

Convert to clausal form

Move ¬ inwards

Answer 32

• ¬∀x ɑ rewrites to ∃x ¬ɑ
• ¬∃x ɑ rewrites to ∀x ¬ɑ

Question 33

Skolemization: idea

for unqualified existential variables

Answer 33

Replace ¬∃x P(x) by P(c) where c is a new constant.

∃y ∀x L(x, y) skolemizes to ∀x L(x, c)

Question 34

Skolemization: idea

for qualified existential variables

Answer 34

If x₁, ... xₙ are the universally quantified variables with scope including ∃x ɑ, then replace all the occurrences of x in ∃x ɑ by f(x₁, ... xₙ) where f is a new function symbol.

∀x ∃y L(x, y) skolemizes to ∀x L(x, f(x))

Question 35

Does skolemization preserve logical equivalence?

Answer 35

No. ∃x P(x) is not logically equivalent to P(c).

Skolemization preserves satisfiability. All we need is to preserve satisfiability for refutation completeness.

Question 36

Substitution

Answer 36

A finite set of pairs {x₁/t₁, ... xₙ/tₙ} where the xᵢ are distinct variables ant the tᵢ are arbitrary terms.

If θ is a substitution and ⍴ is a literal, then θ⍴ is the literal that results from simultaneously replacing each xᵢ in ⍴ by tᵢ.

Question 37

Instance

Answer 37

⍴ is an instance of ⍴' if for some θ, we have θ⍴' = ⍴

Question 38

Most general unifier

Answer 38

θ is an MGU of c₁ and c₂
iff
for any other unifier θ₁ of c₁ and c₂,
then there exists θ₂ such that θ₁=θ₂θ

MGUs are not necessarily unique.

Question 39

MGU algorithm

Answer 39

To find MGU of ⍴₁ and ⍴₂

1. Start with θ={}
2. Exit if ⍴₁ = ⍴₂
3. Otherwise get the disagreement set, DS, which is the pair of terms at the first place where the terms disagree.
4. Find var v∈DS, & term t∈DS not containing v. If not, fail.
5. Otherwise set θ to {v/t} θ and ⍴ᵢ to {v/t} ⍴ᵢ. Go to step 2.

Question 40

2 Reasons the MGU Algorithm might fail

Answer 40

• Clash. A constant variable cannot be changed by any substitution.
• Cyclic. Cannot find v, t, ∈ DS where v does not occur in t.

Question 41

Factoring

Answer 41

Given c₁ ∪ c₂ where |c₂|>1 and θ is an MGU of c₂.

Infer θ(c₁ ∪ c₂)

From [Likes(sam, x), Likes(y, bananas)] Infer [Likes(sam, bananas)]