1. 布林邏輯
2. 謂詞邏輯
3. 一階邏輯

# 推論方法

``````Truth Table Proof Theory
φ is valid iff T╞ φ for the 2^n truth assignment in which validity the n variable of φ appear

Hilbert style proof theory : (logical induction system)
Axiom :
(1) a=>(a=>a)
(2) a=>(b=> a&b)
(3) a&b =>a
(4) a&b =>b
(5) a=> a or b
(6) b=> a or b
(7) (a or b) => ((a=>r)=>((a=>b)=>r))
(8) (a=>b) => ((a=>(b=>r))=>(a=>r))
(9) (a=>b) => ((a=>(-b))=>-r)
(10)--a=>b

Inference Rule :
Modus Ponens :
a, a=>b ==> b

Gentzen style proof theory (Sequent Calculus)
Axiom :
(1) T,φ ├ Δ,φ
(2) T∪{φ} ├ Δ∪{φ}

Inference Rule :

// "," 在左邊表示 &
// "," 在右邊表示 or
// ";" 表示兩式之 &
// 目的：不斷縮短算式的長度。

(&├)                         (├&)
T, a, b ├ Δ                   T ├ a, Δ ; T ├ b, Δ
-----------------------------   ----------------------------
T, a & b ├ Δ                       T ├  a & b, Δ

( or ├)                          (├ or )
T ├ Δ, a; T ├ Δ, b              T ├ Δ, a, b
-----------------------------   ----------------------------
T a or b├ Δ                  T ├ Δ, a or b

(-├)                             (├ -)
T ├ Δ, a                    T, a ├ Δ
-----------------------------   ----------------------------
T, -a ├ Δ                   T ├ Δ, -a

(=>├)                         (├ =>)
T ├ Δ,a; T, b ├ Δ              T, a ├ Δ, b
-----------------------------   ----------------------------
T, a=>b ├ Δ                    T ├  a=>b

(cut rule)
T, a => Δ; T => Δ, a
------------------------- + (cut elimination theorem) = complete.
T => Δ

Sequent : T=>Δ where T,Δ are finite sets of BE's
{φ1,...φn}=>{ci1, ...cim}
Informally we want to capture φ1,...,φn => ci1,...cim

Davis Patumn proof method :

Method : divide and conquer
S
----------------------------
P = true        ;    P = false
S[p = true]        S[p=false]

Case 1 : Unit clauses rule    :    S&{L}  S{Ltrue}
Case 2 : Elimination rule     :    S&{Ci|L}  S
Case 3 : Split rule        :    S  S[Ptrue] ; S[pfalse]

Theorem : S is unsatisfiable iff all sets producted for Davis Patumn are unsatisfiable.
φ = {(p|q) & (-q|s) & (-s|p) & (-p|r) & (-r|-p|t) }  (t & -r)
-φ = (p|q) & (-q|s) & (-s|p) & (-p|r) & (-r|-p|t) & (-t | r)

S
-------------------------------------------------
S[p=true]             ;         S[p=false]
{-q|s, r, -r|t, -t|r}        {q, -q|s, -s, -r | -t}
--------unit clause of r    ----------------unit clause of -s
{-q|s, t, -t}                {q, -q, -r|-t}
-------------                ----------------
false                    false

If there is a P s.t P, -P in S then S is unsatisfiable.

Ground Resolution Proof Theory

Methodology :

To prove that φ is valid, we prove that -φ is unsatisfiable instead.

Inference Rule :

c or x; d or -x
---------------
c or d

Example :

s = { p or q, -p or r, -r or -s or t, q or s, -q , -r or -t}

p or q -p or r
\     /
-r or -t    q or r    -r or -s or t
\  /      \    /
q or -t     q or -s or t
\    /
q or -s    q or s
\   /
q    -q
\   /
False

Completeness of ground resolution theorem :
φ is valid iff NIL can be deduced from S using ground resolution.
Proof :
Given a set of propositional variable {p1, ..., pn}
A semantic tree is
S
T        F            p1
T       F  T        F        p2
P3…

Each nodes represents is a partial interpretation of the variables assigned so far,
where values are indicated as labeled as the edges.

If S is unsatisfiable,
S=c1&c2&...&cn
Then each ci is a false

A tree in which all pathes ends in a falsified node is called a closed semantic tree.

Proposition : If S is unsatisfiable then one can get a closed semantic tree no matter
how the variable are ordered.

Proof of proposition
Choose the (longest) path from the closed semantic tree.

/
/ \
T          F
D|-P        C|P
Then ground resolution will produce C|D
By induction , ground resolution is complete.

Refinement 1 : Ordered ground resolution
(assumed there is an ordering on variable, any order is good)
If P is the longest atom assigning, C|P & D|-P  C|D

Refinement 2 : Positive ground resolution
(Choose the rightest path with all positive asignment)

Refinement 3 : positive ordered ground resolution
(Choose the all positive clause with longest path)

The Refinement doesn't means that the produced proof will be shorter than resolution.
It means that the choosing space of each step is small than the resolution case.

My Refinment : Shortest first ground resolution

My Refinment : Prune the other branch that is not needed any more.
P|-q     prune the -p&q```
```