Proof Flashcards
1
Q
Meaning of A ⊨ B
A
A ⊨ B means that B is true in every structure in which A is true.
2
Q
Meaning of A ⊢ B
A
A ⊢ B means B can be proved using A as the premises.
3
Q
Soundness
A
If A ⊢ B then A ⊨ B
4
Q
Completeness
A
If A ⊨ B then A ⊢ B
5
Q
reductio ad absurdum
A
An assumption is rejected because it leads to a contradiction (an absurdity).
6
Q
AND introduction
A
7
Q
AND elimination
A
8
Q
OR Introduction
A
9
Q
OR Elimination
A
10
Q
NOT Introduction
A
11
Q
NOT Elimination
A
12
Q
IMPLIES Introduction
A
13
Q
IMPLIES Elimination
A
14
Q
Double negation elimination
A
15
Q
Excluded middle
A
⊢ A ∨ ¬A
16
Q
Universal Elimination
A
- We know that for all
xthe statementpholds. - We have a term
tthat we need to use in our argument. - So we know that the statement
pholds if we replacexbyteverywhere in the statement.
17
Q
Universal introduction
A
- We are using
xfor a completely arbitrary element of the domain, being careful not to assume it has any special properties. - We show that
xhas to have the property stated in the formulap. - Because
xwas arbitrary, we conclude that the formulapmust hold for allx.
18
Q
Existential elimination
A
- We know there is some
xwith the property stated byp. - Let’s introduce a new name,
a, for a particular thing with this property. - We deduce that some statement,
s, (not involvinga) must hold by an argument using the assumption thatahas propertyp. - We conclude that
sholds on its own, without the assumption aboutahaving propertyp.
19
Q
Existential introduction
A
- We have a statement
pabout some particular termt. - We conclude that there is some x with the property stated by
pwhere we replacetbyx.
20
Q
literal
A
A WFF which is either an atom (an atomic proposition) or the negation of an atom.
21
Q
Clause
A
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
22
Q
Horn clauses
A
Clauses with at most one positive literal.
23
Q
Equivalent clause to false
A
Empty clause[]
24
Q
Equivalent disjunction to a → b
A
¬a ∨ b
25
Clausal resolution
`α` is an atom
`Σ₁` and `Σ₂` are clauses
`α` is called the **atom resolved upon**.
`Σ₁` and `Σ₂` is the **resolvent**.
26
Procedure for reduction to CNF
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 )`
27
Clausal Form
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.
28
Equivalent clause to true
Empty conjunction
{ }
29
Resolution Refutation Procedure
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.
30
Resolution in first-order logic
- Convert knowledge base and negated query to clauses
- Keep resolving until get empty clause or cannot continue
31
Convert to clausal form: first order case
**6 Steps**
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.
32
# Convert to clausal form
Move `¬` inwards
- `¬∀x ɑ` rewrites to `∃x ¬ɑ`
- `¬∃x ɑ` rewrites to `∀x ¬ɑ`
33
Skolemization: idea
| for unqualified existential variables
Replace `¬∃x P(x)` by `P(c)` where `c` is a new constant.
| `∃y ∀x L(x, y)` skolemizes to `∀x L(x, c)`
34
Skolemization: idea
| for qualified existential variables
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))`
35
Does skolemization preserve logical equivalence?
No. `∃x P(x)` is not logically equivalent to `P(c)`.
Skolemization preserves **satisfiability**. All we need is to preserve satisfiability for refutation completeness.
36
Substitution
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ᵢ`.
37
Instance
`⍴` is an instance of `⍴'` if for some `θ`, we have `θ⍴'` = `⍴`
38
Most general unifier
`θ` is an MGU of `c₁` and `c₂`
iff
for any other unifier `θ₁` of `c₁` and `c₂`,
then there exists `θ₂` such that `θ₁`=`θ₂θ`
## Footnote
MGUs are not necessarily unique.
39
MGU algorithm
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.
40
2 Reasons the MGU Algorithm might fail
- `Clash`. A constant variable cannot be changed by any substitution.
- Cyclic. Cannot find `v, t, ∈ DS` where `v` does not occur in `t`.
41
Factoring
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)]`
