计算机数理逻辑-命题逻辑-归结

The method of resolution is an efficient method for searching for a proof.

1. Reasoning Methods

• Resolution
• DPLL/CDCL
• Tableaux

A refutational reasoning反驳性推理 method (or just reasoning method RM) is an algorithm (not necessarily terminating) which given as an input a set of formulas S outputs either “satisfiable”, “unsatisfiable” or “don’t know”

• 区别于decision procedure: True / False

1.1. Soundness

Consider a set of formulas Φ (usually called a fragment).
A reasoning method RM is sound for Φ if for any set S ⊆ Φ:

• if RM(S) is “satisfiable” then there is an interpretation satisfying all formulas in S
• if RM(S) is “unsatisfiable” then there is no interpretation satisfying all formulas in S.
• A trivial琐碎 RM which on all inputs returns “don’t know” is a sound reasoning method

1.2. Completeness

A reasoning method RM is (refutationally) complete for Φ if for any set
S ⊆ Φ:

• if S is unsatisfiable then RM(S) is terminating and returns “unsatisfiable”

1.3. Refutation completeness

A formal system $S$ is refutation-complete if it is able to derive false from every unsatisfiable set of formulas. That is,

• $\Gamma \models _{\mathcal {S}}\bot \to \ \Gamma \vdash _{\mathcal {S}}\bot$
  • 也就是unsat的表达方式为$\Gamma \models \bot$

This is sufficient since $T⊢A$ is equivalent to $T∪ { ¬A }⊢⊥$. So if we want to see a formula $A$ is derivable from $T$, we only need to check if there is a refutation proof for $T∪{ ¬A }$ which can be checked using resolution.

1.4. Trivialism 琐碎论

• 琐碎论是一承认所有语句（也称为命题）为真并且所有“P与非P”形式的矛盾句都为真的逻辑理论
• P当且仅当P为真

2. Clause 子句

Clause: a disjunction析取 $L_1 ∨ . . . ∨ L_n$, n ≥ 0 of literals.

• A clause can be seen as a mulit-set of literals ${ L_1, . . . , L_n }$
• Empty clause, denoted by ⊥: n = 0(also denoted as □, the empty clause is false in every interpretation)
• Unit clause单位子句: n = 1
  • A clause is unit under a partial assignment when that assignment makes every literal in the clause unsatisfied but leaves a single literal undecided
  • 如果一个子句中，除了一个未决定的字面量，所有字面量都已经确定为假，我们就称这个子句为“单位子句”
• Trivial Clauses
  • clause if trivial if it contains a pair of clashing冲突的 literals. 
  • Since a trivial多余 clause is valid ($p∨¬ p ≡ T$), it can be removed from a set of clauses without changing the truth value of the formula.
• A formula is considered to be an implicit conjunction of its clauses
  • ${ L_1 \lor … \lor L_n } \land { L_1 \lor … \lor L_n }$
• The formula that is the empty set of clauses is denoted by $∅$.

2.1. Horn Clauses 霍恩子句

霍恩子句（Horn Clause）是带有最多一个肯定文字的子句

• 一个霍恩子句的例子：${\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}$
• 它可以被等价地写为：${\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u}$

3. Conjunctive Normal Form 合取范式

写成合取范式的公式由一些子句（clause）相与（AND, $\lor$()）而成；子句则是由字面量（literal）相或（OR, $\land{}$) 而成；每个字面量就是一个变量，或者由变量 取非($\lnot{}$) 得到

• 由于这样的公式只是一些子句“与”起来，为使公式满足，每个子句也都必须得到满足；
• 由于每个子句只是一些字面量“或”起来，只要满足了一个字面量就满足了整个子句

A formula is in conjunctive normal form (CNF) iff it is a conjunction of disjunctions of 字面量literals

• 在布尔逻辑中，如果一个公式是子句clause的合取(conjucntion)

• Every formula in propositional logic can be transformed into an equivalent formula in CNF

• A formula is in 3CNF iff it is in CNF and each disjunction has exactly three literals.

推导例子

• 也就是公式形式vs集合形式

• Clausal form of a formula A: a set of clauses which is satisfiable if and only if A is satisfiable.

• Clausal form of a set S of formulas: a set of clauses which is satisfiable if and only if so is S.

3.1. Definitional Clausal Form Transformation

• CNF cannot avoid exponential blowup指数爆炸
  • Approach: relax requirement of equivalence preserving to equisatisfiability preserving
  • 也就是重命名（比如n=$p_1\leftrightarrow{p_2}$）
• structure CNF

1. Take all subformulas that are not literals. （见subformula定义）
2. Introduce names for these formulas. Note we do not introduce names for literals.
3. Introduce definitions.
4. Convert resulting formulas into CNF using the standard transformation

4. Resolution Rule 归结原理

Propositional Resolution inference system BR, consists of the following inference rules

• Resolution rule也就是Inference rule

example

4.1. Tree vs Linear

5. inference 推理

• premises前提: known or assumed to be true
• conclusion结论
• An inference rule R is a set of inferences.
• An inference system, (or a calculus演算) I is a set of inference rules.

5.1. sound

• An inference system is sound if all its inference rules are sound
• If an inference system $I$ is sound then for any set of formulas S:
  • $S ⊢_I ⊥$ implies $S ⊨ ⊥$

5.2. completeness

• An inference system $I$ is refutationally complete if for any set of formulas S we have
  • $S ⊨ ⊥$ implies $S ⊢_I ⊥$
  • 亦即Refutation completeness

6. Simplification rules 化简规则

to remove clauses in the saturation process without affecting neither soundness nor completeness

6.1. derived and saturated

• ⊥ is derived == $⊥ ∈ S_n$ for some n
• no new clauses can be derived from S and ⊥ ̸∈ S, then S is saturated; in this case S is satisfiable

6.2. Rule: Tautology elimination (TE)

• S ⇒ S \ {C}
  • where C is a tautology (⊨ C)

6.3. Rule: Subsumption Elimination (SE)

• A clause C subsumes归入 a clause D if C ⊂ D

• S ⇒ S \ {D}

  • where there is C ∈ S such that C ⊂ D

• We say a clause C to is in a set-reduced form if every literal occurs no more than once in C. A clause C in a set-reduced from can be seen as a set of literals (rather than a multi-set).
• BR with eager (BF) and (SE) is a decision procedure for propositional logic

也就是说SE就是把整个式子消减了，之后的推理不能再用这个式子了

7. Inference vs Deductive vs Resolutuion 推论vs演绎vs归结

• We use reasons or reasoning to form inferences which are basically conclusions drawn from propositions or assumptions that are supposed to be true.
  • 推论是从假定为真实的命题(前提)得出的结论
• Deduction is a general-to-specific form of reasoning that goes from known truths to specific instances. It starts with a hypothesis and examines the possibilities within that hypothesis to reach a conclusion. Example, in chemistry deducing a chemical equation basis two or more agents.
  • 演绎是一种从一般到具体的推理形式，从已知真理到具体实例
  • 它从一个假设开始，研究该假设中的各种可能性以得出结论
• resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic
  • 归结是一种反向证明的方法，是对于命题逻辑和一阶逻辑中的句子的推理规则