Formal System-表达逻辑:Syntax，Semantik

两个例子

看一下怎么用表达逻辑描述问题

数独问题

用Dki,jD_{i,j}^k∈(true,false)\in{(true,false)}表示第i行，第j列的数值为k是真的或假的。

那么数独的规则则可以如下描述 :

1.每行至少出现一个1:(只写第一行，列与区域以此类推)

D11,1∨D11,2∨D11,3∨D11,4∨D11,5∨D11,6∨D11,7∨D11,8∨D11,8D_{1,1}^1\lor D_{1,2}^1\lor D_{1,3}^1\lor D_{1,4}^1\lor D_{1,5}^1\lor D_{1,6}^1\lor D_{1,7}^1\lor D_{1,8}^1\lor D_{1,8}^1

2.每行最多出现一个1:

这个就饶了我吧，太长了，思路是：1所在位置有9种可能性那么就把他们并起来吧

1在第一格的描述如下：

D11,1∧¬D11,2∧¬D11,3∧¬D11,4∧¬D11,5∧¬D11,6∧¬D11,7∧¬D11,8∧¬D11,8D_{1,1}^1\land \lnot D_{1,2}^1\land \lnot D_{1,3}^1\land \lnot D_{1,4}^1\land \lnot D_{1,5}^1\land \lnot D_{1,6}^1\land \lnot D_{1,7}^1\land \lnot D_{1,8}^1\land \lnot D_{1,8}^1

3.每个格最多只能有一个数字，表示如下

¬(Dsi,j∧Dti,j)\lnot(D_{i,j}^s \land D_{i,j}^t)

其中1<=i,j,s,t<=9并且s

八皇后问题

呵呵

表达逻辑的基本概念

逻辑标志:1,0,¬\lnot,∧\land,∨\lor,→\to,↔\leftrightarrow,(,)

Signatur:Symbol(Atom)的集合，用∑\sum表示

Formel:表示为For0∑For0_{\sum}即公式的意思，包括1,0,∑\sum,及∑\sum中的各种运算如：非，交，并等

Interpretation:关于∑\sum的一个interpretation就是任意的到｛true，false｝上的映射

表示为I:∑→\sum \to{ture,false}

取值(Auswertung):每个针对∑\sum的Interpretation都有一个确定的取值，表示为：

valI:For0∑→val_I: For0_{\sum} \to{true,false}

Modell:Formel A ∈For0∑\in For0_{\sum},当一个针对∑\sum的Interpretation I 满足valI(A)=Wval_I(A) = W. 就说这个Interpretation是Formel A的一个Modell

普遍正确(Allgemeingueltig):A∈For0∑A \in For0_{\sum}被称为普遍正确的，当对所有的Interpretation有valI(A)=trueval_I(A)=true.

可实现(Erfuellbar)A∈For0∑A \in For0_{\sum}被称为可实现的，当存在一个Interpretation可以实现valI(A)=trueval_I(A)=true.

M⊨AM \vDash A:有M可以退出A，即M的任意一个Modell同时也是A的Modell。

例子:一些普遍正确的Formeln

A→AA \to A //Selbstimplikation

¬A∨A\lnot A \lor A //Tertium non datur

A→(B→A)A \to (B \to A) //Abschwaechung 这个可以有

0→A0 \to A //Ex falso quodlibet

(A∧(A→B))→B(A \land (A \to B)) \to B //Modus Ponens 呵呵了

A∧A↔AA \land A \leftrightarrow A //Idempotenz

(¬¬A)→A(\lnot \lnot A) \to A //Doppelnegation

A∧(A∨B)↔AA \land (A \lor B) \leftrightarrow A //Absorption

(A↔B)↔((A→B)∧(B→A))(A \leftrightarrow B) \leftrightarrow ((A \to B) \land (B \to A)) //Aequivalenz/Implikation

A∧(B∨C)↔(A∧B)∨(A∧C)A \land (B \lor C) \leftrightarrow (A \land B) \lor (A \land C) //Distributivitaet

A∨(B∧C)↔(A∨B)∧(A∨C)A \lor (B \land C) \leftrightarrow (A \lor B) \land (A \lor C) //Distributivitaet

//以上Formeln可通过转换(umformen)或真值表来证明

几个重要的定理

A 可实现 ↔¬A\leftrightarrow \lnot A普遍正确 //一般用于证明可实现

⊨A↔\vDash A \leftrightarrow A 普遍正确 //即∅⊨A\varnothing \vDash A空集恒真

⊨¬A↔\vDash \lnot A \leftrightarrow A 不可实现

A⊨B↔⊨A→BA \vDash B \leftrightarrow \vDash A \to B

M∪A⊨B↔M⊨A→BM \cup {A} \vDash B \leftrightarrow M \vDash A \to B

Boolesche Funktionen

就是公式表达式，包括了定义和完备性(Vollstaendigkeit)的说明

Craigsch插值定理(Craigsche Interpolationslemma)

A,B 为AL Formeln并且有 ⊨A→B\vDash A \to B那么就存在C满足⊨A→C且⊨C→B\vDash A \to C 且 \vDash C \to B(C中的Atom不能超出A, B的范围)。这个C就是我们的插值。

那么如何快速的找到这个插值呢，因为插值无论真假对原式并无影响，所以用一下方法找到插值：

假设P1,...PnP_1,...P_n为在A中出现当却不在B中出现的Atom，从A出发我们通过使用cic_i 代替PiP_i构建新的Formeln称为A[c1,...,cnc_1,...,c_n]，其中ci∈c_i \in {1,0}，如此我们可以得到插入值：

C≡⋁(c1,...,cn)∈(1,0)nA[c1,...,cn]C \equiv \bigvee_{(c_1,...,c_n) \in (1,0)^n} A[c_1,...,c_n]

简单的例子

A=P1∧P2,B=P1∨P3A = P_1 \land P_2, B = P_1 \lor P_3

那么P2P_2是A中的Atom，而没出现在B中

A[1]=P1∧1↔P1A[1]=P_1 \land 1 \leftrightarrow P_1

A[0]=P1∧0↔0A[0]=P_1 \land 0 \leftrightarrow 0

C=A[1]∨A[0]↔P1C = A[1] \lor A[0] \leftrightarrow P_1

所以P1P_1就是插值

//这是P只有一个时的情况所以看起来这方法还是相当不错的

//但是其实这个方法的实用性并不高，因为随着P的数目的增加，A[]的数目呈现指数增长。