邏輯推論

導論篇

計算理論簡介

計算理論的歷史

可計算性

可計算性簡介

圖靈機

不可計算問題

遞歸可枚舉

不完備定理

複雜度

複雜度簡介

複雜度理論

NP-Complete

隨機複雜度

密碼學理論

趨近演算法

訊息

相關網站

參考文獻

最新修改

簡體版

English

邏輯系統

  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 => Δ
若我們把 cut rule 用 (-├) 移位,則 cut rule 變成 T, a, -a ├ Δ

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

Facebook

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License