Logic of automatic reasoning 09 - automatic theorem proving

Logic of automatic reasoning 09– Automatic theorem proving

Summary of proposition analysis

C ∨ ϕ 		C′ ∨ ¬ϕ
---------------------
		C ∨ C'

Applicable to the conjunctive paradigm (CNF) The formula expressed
Used to refute theorem proof （ Prove that your opposite desire is insatiable ）.
The goal is to export □（ Empty clause ）. This shows unsatisfiability .

summary
Parsing can be extended to predicate logic
But it does not produce a decision-making process （ Predicate logic is undecidable ）
But first of all, for Propositional Analysis , We need to put the formula into the conjunctive normal form . Again , We need to bring first-order sentences into the clause paradigm .

rename Renaming
If no variables appear in the formula at the same time, and if different quantifiers appear, bind different variables , The formula is renamed
Each formula is equivalent to a renamed formula
From here on, we assume that all formulas are renamed
(∀x.[ P(x) ∧ ∀x.Q(x) ]) → R(x) Equivalent to a renamed formula (∀x.[ P(x) ∧ ∀y.Q(y) ]) → R(z)

Negative paradigm Negation Normal Form
Whether a formula has a normal form , If and → It doesn't appear in it, and every negative symbol immediately precedes an atomic formula
Each formula is equivalent to the formula in the negative paradigm
prove ： Use CNF The rules , Add the negative paradigm
¬∀x.φ ≡ ∃x.¬φ
¬∃x.φ ≡ ∀x.¬φ
¬¬∀a.¬P(a) Not a negative paradigm

Prenex normal form
The formula of predicate logic is prenex normal form , If it is form Q1x1 . . Qnxn.φ about Qi ∈ {∀, ∃} and φ Is quantifier free
Each renamed formula is equivalent to prenex Formulas in the normal form
prove ： Rename to ensure x stay ψ China is not free , Then rewrite ：

(∀x.φ) ∧ ψ ≡ ∀x.(φ ∧ ψ)
(∀x.φ) ∨ ψ ≡ ∀x.(φ ∨ ψ)
(∃x.φ) ∧ ψ ≡ ∃x.(φ ∧ ψ)
(∃x.φ) ∨ ψ ≡ ∃x.(φ ∨ ψ)
(∀x.φ) ∧ (∀y.ψ) ≡ ∀x.(φ ∧ ψ)
(∃x.φ) ∨ (∃y.ψ) ≡ ∃x.(φ ∨ ψ)

Prenex normal form ： Abstract
prenex The normal form algorithm has the following steps ：
step 1 Rename formula
step 2 Transform into a negative paradigm
step 3 Use the above equivalence to pull all quantifiers to the front
Be careful ： We assume by default that prenex nf The formula in is also negating nf in

(¬∃x.P(x)) ∧ (∃y.Q(y) ∨ ∀z.P(z))
	≡ (∀x.¬P(x)) ∧ ∃y.(Q(y) ∨ ∀z.P(z))
	≡ ∃y.((∀x.¬P(x)) ∧ (Q(y) ∨ ∀z.P(z)))
	≡ ∃y.((∀x.¬P(x)) ∧ ∀z.(Q(y) ∨ P(z)))
	≡ ∃y∀z.((∀x.¬P(x)) ∧ (Q(y) ∨ P(z)))
	≡ ∃y∀z∀x.((¬P(x)) ∧ (Q(y) ∨ P(z)))

Scholemanization Skolemisation
Next we want to delete the quantifier prefix
This transformation preserves （ No ） Satisfiability , But equivalence is not preserved
One formula is Skolem normal form , If it is prenex Paradigm and contains only full quantifiers
In the algorithm, , We use new Skolem Function and constant substitution ∃

∀x1 . . . ∀xn∃y.φ 	⇝ 	∀x1 . . . ∀xn. φ[f (x1, . . . , xn)/y]
			∃y.φ 	⇝ 	φ[c/y]

Scholemanization ： Intuitive explanation intuitive explanation
Consider the statement ∃x.P(x)：
If this is satisfiable , Then there must be some value c bring P establish .
We are not from the general statement ∃x.P(x) Reasoning , But reasoning from the facts P. We leave it to others to calculate c What is it? .
Similarly , If ∀x.∃y.P(x, y) Is satisfiable ：
This means that whenever someone gives us a value x when , There must be some corresponding values y send P(x, y) Work . We can say y = f (x) For some functions that we worry about f.
We will ∀x.∃y.P(x, y) Replace with ∀x.P(x, f (x)) And infer accordingly .

Example
Given ∃x.(¬P(a) ∨ P(x)), With a new “Skolem constant ”c Replace x Make the formula work . This gives ¬P(a) ∨ P. [ The first formula is valid ; This second can only satisfy .]

Skolemising ∃x.∀y.∃z.P(x, y, z) yield
	∃x.∀y.∃z.P(x, y, z)
⇝ ∃x.∀y.P(x, y, f (y))
⇝ ∀y.P(c, y, f (y))

among c It's a new one “Skolem constant ”, and f It's a new dollar “Skolem function ”.

Before we explain f Before , We need to know what model we are using .
∀m.∃n.(m < n) ⇝ ∀m.(m < f (m))
among f It's a new dollar Skolem function .
hypothesis < Express in natural numbers “ Less than ”, We can take f (m) = m + 1;
hypothesis < In set theory “ Appropriate subset ”, We can do anything c ̸∈ m take f (m) = m ∪ {c}

	¬∃a.∀b.(a ≤ b) 		need to move ¬
⇝ ∀a.¬∀b.(a ≤ b) 		need to move ¬
⇝ ∀a.∃b.¬(a ≤ b) 		replace b with f (a)
⇝ ∀a.¬(a ≤ f (a)) 		now in Skolem nf

In natural number , This is different from saying ∀a.(f (a) < a) identical . This cannot satisfy the natural number , Because take a = 0 Will give f (a) < 0, That is impossible . therefore , The original statement is invalid .

Clause paradigm Clause Normal Form
stay Scholemanization after , We can also get rid of the full quantifier
The formula in the clause paradigm is essentially CNF The formula , The text is the atomic formula of predicate logic
We write for the clause paradigm CNF, by Skolem Normal form writing SNF
Clause normal form algorithm
The first 1 Step ： With prenex Form introduction formula
step 2：skolemise, Then delete the full quantifier
The third step ： Turn into CNF

	∃a.∀b.((∃c.c < b) → ¬(b = a)) 		need to remove →
⇝ ∃a.∀b.(¬(∃c.c < b) ∨ ¬(b = a)) 		need to move ¬
⇝ ∃a.∀b.((∀c.¬(c < b)) ∨ ¬(b = a)) 	now in negation nf
⇝ ∃a.∀b.∀c.(¬(c < b) ∨ ¬(b = a)) 		now in prenex nf
⇝ ∀b.∀c.(¬(c < b) ∨ ¬(b = z)) 			now in Skolem nf
⇝ ¬(c < b) ∨ ¬(b = z) 					now in cnf

Unified Unification
We try to apply resolution in a more general form

 C ∨ L      C'' ∨ L''
 -------------------------
 	(C ∨ C'')σ

σ It's replacement , bring Lσ = L’σ and C ∨ L, C′ ∨ ¬L’ Was renamed .
Be careful ： It is customarily written Cσ instead of σ
Example (Given σ = {p 7→ baby, q 7→ baby}, we have)
{Loves(p, baby)}σ = {Loves(baby, baby)} = {Loves(baby, q)}σ
{Loves(p, baby)} and {¬Loves(baby, q), q = me} are renamed.
Therefore:

{
    Loves(p, baby)} 	{
    ¬Loves(baby, q), q = me}
------------------------------------------------
			{
    q = me}σ

The most common unifier (mgu)
Give Way s and t Become a term
If sσ = tσ, The replacement σ yes s and t The unifier of
Unifier σ yes s and t The most general unifier of (mgu) If for all unifiers ρ Of s and t There is a substitution τ bring ρ = τ ◦ σ
Intuitively , Any unification of the two terms can be derived from their mgu By further instantiation
It can be proved that any two terms have one mgu

Example
f (g(x, b), f (x, z)) and f (y, f (g(a, b), c)) Of mgu How much is the ？
They are all f (arg1, arg2) In the form of .
Unify the two arg2 need f (x, z) ≈ f (g(a, b), c). This in turn requires x |→ g(a, b) and z |→ c. Unify the two arg1 need y |→ g(x, b), Where the transformation maps to g(g(a, b), b), because x |→ g(a, b). Putting these bits together gives us a unified example f (g(g(a, b), b), f (g(a, b), c))

Unified algorithm Unification Algorithm
We also calculate the set mgu≈ t1,…sn≈ tn, We want to find one σ, It will simultaneously put each si And the corresponding ti Unite . We write E For such sets and E,s ≈ t about E ∪ {s ≈ t}
Unified algorithm ： Apply these rules

E,s 				≈ s ⇝ E
E, f (s1, . . . ,sn) ≈ f (t1, . . .tn) ⇝ E,s1 ≈ t1, . . .sn ≈ tn
E, f (. . .) 		≈ g(. . .) ⇝ ⊥
E,t 				≈ x ⇝ E, x ≈ t 			if t ̸∈ V
E, x 				≈ t ⇝ ⊥ if x ̸= t, x ∈ V(t)
E, x 				≈ t ⇝ E[t/x], x ≈ t 		if x ∈ V(E), x ̸∈ V(t)

Unified algorithm ： How it works
E,s ≈ s ⇝ E
Everything always looks like itself . So there is no need to do anything to s ≈ s.
E, f (s1, … ,sn) ≈ f (t1, … .tn) ⇝ E,s1 ≈ t1, … . .sn ≈ tn
If you match two applications with the same function , It's enough to match the parameters
E, f (. . .) ≈ g(. . .) ⇝ ⊥
You can't unify different constants 、 Functions, etc .

Example （ Can be unified ）

	f (g(x, b), f (x, z)) ≈ f (y, f (g(a, b), c))
⇝ g(x, b) ≈ y, f (x, z) ≈ f (g(a, b), c)
⇝ y ≈ g(x, b), x ≈ g(a, b), z ≈ c
⇝ y ≈ g(g(a, b), b), x ≈ g(a, b), z ≈ c

Example （ It can't be unified ）

	f (x, x) ≈ f (a, b)
⇝ x ≈ a, x ≈ b
⇝ b ≈ a, x ≈ b
⇝ ⊥

Analysis of predicate logic Resolution for Predicate Logic
The analytic reasoning rule of predicate logic is

	 C ∨ L      C'' ∨ L''
	 -------------------------
	 	(C ∨ C'')σ
 σ = mgu(L, L′)

In all applications , The site must be renamed ： Their variables must be disjoint
however , This rule alone does not completely refute ：
Γ = { {P(x), P(y)}, {¬P(a), ¬P(b)}} Unsatisfiable
but Γ All clauses in Γ∗ There are at least two literal quantities
therefore □ It cannot be calculated by resolution alone

To overcome this kind of problem , We sometimes need to use factorization . This means using inference rules ：

	 C ∨ L      C'' ∨ L''
	 -------------------------
	 	(C ∨ C'')σ
 where σ = mgu(L, L′)

Since {
    P(x), P(y)} ≡ (⊥ ∨ P(x) ∨ P(y)) and mgu(P(x), P(y)) = {
    y 7→ x}:
				P(x) ∨ P(y)
				------------(factoring)
					P(x)

we can rewrite ∀x.∀y.(P(x) ∨ P(y)) as ∀x.P(x).

Example 1
negating H(s) ∧ ∀x. (H(x) → M(x)) → M(s) and computing CNF yields
{ {H(s)}, {¬H(x), M(x)}, {¬M(s)}}
Then we can use the resolution to deduce □
The use of mgu yes x |→ s
Therefore, the initial formula is valid

Example 2
negating ∃y∀x. P(x, y) → ∀x∃y. P(x, y) and computing CNF yields{ {P(x, a)}, {¬P(b, y)} with fresh Skolem constants a and b
We can use resolution to derive □
The use of mgu yes x |→ b, y |→ a,
Therefore, the initial formula is valid

Example 3
proving the drinker paradox ∃x. (P(x) → ∀y. P(y)) with natural deduction is hard negating, computing the CNF and renaming yields { {P(x)}, {¬P(f (y))}}
that mgu x |→ f (y) The resolution of proved to be negligible
Rename for derivation □ Is essential
Last , This is a proof that requires factorization

Soundness and integrity Soundness and Completeness
It is easy to prove that the parsing of predicate logic is reasonable ：
A subset of sentences is unsatisfiable , If its saturation contains □
In order to refute the integrity , We need to know whether all ground instance solving steps are instances of non ground steps ：
if C1, C2 It has disjoint variables and basic instances C Clause of C1’, C2 ' This can be solved as C’ Through the ground resolution , be C1,C2 Can be broken down into C and C’ yes C An example of
If a subset of sentences is unsatisfiable , Then its saturation contains □

Automatic proof search ： Partial summary
Resolution based theorem proving combines logic with a powerful rewriting process
Eliminate redundant clauses to maintain the set Γ Small
Decades later , Automatic proof search is still an active research field