查看“︁归结原理”︁的源代码

{{NoteTA
|G1=IT}}

'''归结'''（resolution）原理，在[[数理逻辑]]和[[自动定理证明]]中（[[GOFAI]]涉及的主题），是对于[[命题逻辑]]和[[一阶逻辑]]中的句子的[[推理规则]]，它导致了一种[[反证法]]的[[定理]][[证明]]技术。

== 命题逻辑中的归结 ==

=== 归结规则 ===

在命题逻辑中的'''归结规则'''是一个单一的有效的[[推理]]规则，从两个[[子句 (逻辑)|子句]]生成它们所蕴含的一个新的子句。归结规则接受包含互补的文字的两个子句 - 子句是[[文字 (数理逻辑)|文字]]的析取式，并生成带有除了互补的文字的所有文字的一个新子句。形式上，这里的<math>a_i</math>和<math>b_j</math>是互补的文字：

<math>\frac{
a_1 \lor \ldots \vee a_{i-1} \vee a_i \vee a_{i+1} \vee \ldots \lor a_n, 
\quad b_1 \lor \ldots \vee b_{j-1} \vee b_j \vee b_{j+1} \vee \ldots \lor b_m}
{a_1 \lor \ldots \lor a_{i-1} \lor a_{i+1} \lor \ldots \lor a_n  \lor  b_1 \lor \ldots \lor b_{j-1} \lor b_{j+1} \lor \ldots \lor b_m}</math>

归结规则生成的子句叫做两个输入子句的''归结''（resolvent）。

当两个子句包含多于一对的互补文字的时候，归结规则可以（独立的）应用到每个这种文字对上。但是，只有要消去（resolve）的文字对可以去除：所有其他文字对仍保留在归结后的子句中。

=== 一种归结技术 ===

当外加上完备的[[搜索算法]]的时候，归结规则生成一个可靠的和完备的算法来决定命题公式的''可满足性''，并且经过扩展，决定句子在一组公理下的有效性。

这种归结技术使用[[反证法]]，并基于在命题逻辑中的任何句子都能转换成等价的[[合取范式]]句子的事实。步骤如下：
* 在知识库中所有句子和要证明的句子（''猜测''（conjecture）)的''否定''都合取连结。
* 结果的句子变换成合取范式（处理成一组子句）。
* 把归结规则应用到包含互补的文字的所有可能的子句对，通过除去重复的文字来简化结果的句子。如果句子包含互补的文字，则（作为[[重言式]]）丢弃它。如果没有，并且它在子句的集合中仍然不存在，则增加上它，并考虑做进一步的归结推理。
* 如果在应用归结规则之后推导出''空子句''，则全部的公式是不可满足的（或者说''矛盾的''），所以可以做出最初的猜测从这些公理中推出的结论。
* 在另一方面，如果不能推导出空子句，并且不能应用归结规则推导更多的新子句，则这个猜测不是最初的知识库的定理。

这个算法的一个实例是最初的[[Davis-Putnam算法]]，它后来被精制成去除了对归结出的子句的显式表示的需求的[[DPLL算法]]。

== 一阶逻辑中的归结 ==
一阶逻辑归结把传统的[[推理规则|逻辑推理]]的[[直言三段论]]浓缩成了一个单一的规则。

要理解归结是如何工作的，考虑[[词项逻辑]]三段论的下列例子：

:所有希腊人都是欧洲人。
:荷马是希腊人。
:所以，荷马是欧洲人。

或者，更一般性的：

: ∀X, P（X）→ Q（X）。
: P（a）。
:所以, Q（a）。

要使用归结技术重造推理，首先子句们必须转换成[[合取范式]]。在这种形式下，所有的[[量化]]都成为隐含的：在变量（X, Y...）上的[[全称量词]]理所当然的被省略了，而[[存在量化]]的变量被替换成[[Skolem函数]]。

: ¬P（X）∨ Q（X）
: P（a） 
:所以, Q（a）

所以，问题是归结技术如何从前两个子句推导出最后一个子句?规则是简单的：

* 找到包含相同谓词的两个子句，这个谓词在一个子句中是否定的而在另一个子句中是肯定的。
* 在两个谓词上进行[[合一]]。（如果合一失败，则你做了错误的谓词选择，回到前面的步骤再次尝试。）
* 如果在被合一的谓词中受到约束的任何未绑定的变量也出现这两个子句中的其他谓词中，则同样的把它们替换（replace）成它们的绑定值（项）。
* 丢弃被合一的谓词，并合并两个子句中的余下的谓词到一个新子句中，并用"∨"算子连接起来。

要应用这个规则到上述例子，我们找到谓词P以否定形式出现在第一个子句中

: ¬P（X）

并以非否定形式出现在第二个子句中

: P（a）

X是一个未绑定变量，而a是一个绑定变量（原子）。合一两个子句生成代换（substitution）

: X := a

丢弃合一了的谓词，并把这个代换应用到余下的谓词中（在本例中就是Q（X）)，生成结论：

: Q（a）

举个其他例子，考虑三段论形式

:所有克里特岛人都是岛上居民。
:所有岛上居民都是说谎者。
:所以，所有克里特岛人都是说谎者。

或者更一般性的,

: ∀X P (X) → Q（X）
: ∀X Q (X) → R（X）
:所以, ∀X P (X) → R（X）

在合取范式中，前提变成了：

: ¬P（X）∨ Q（X）
: ¬Q（Y）∨ R（Y）

（注意在第二个子句中的变量被重命名来使在不同子句中的变量清晰的区分开来。）

现在，合一第一个子句中的Q（X）和第二个子句中¬Q（Y）意味着X和Y变成了同一个变量。把这个变量代换到余下的子句中，合并它们给出结论：

:  ¬P（X）∨ R（X）

归结规则（带有额外的[[因数分解]]）同样的包容传统逻辑的所有其他的演绎形式。

== Paramodulation ==
Paramodulation是一种相关技术，用于推理条款集，其中[[謂詞變量]]是平等的。它可以生成所有 "相等 "的子句，但反身的相同性除外。参数化操作需要一个正的''从''子句，它必须包含一个平等字面。然后，它搜索一个 "进入 "子句，该子句与平等关系的一方相统一。然后，该子项被等号的另一边所取代。Paramodulation的一般目的是将系统简化为原子，在替换时减少术语的大小。<ref name="Rubio">{{cite book|chapter=Paramodulation-Based Theorem Proving|title=Handbook of Automated Reasoning|first1=Robert|last1=Nieuwenhuis|first2=Alberto|last2=Rubio|url=http://www.cmi.ac.in/~madhavan/courses/theorem-proving-2014/reading/Nieuwenhuis-Rubio.pdf|access-date=2022-03-21|archive-date=2021-12-31|archive-url=https://web.archive.org/web/20211231222606/https://www.cmi.ac.in/~madhavan/courses/theorem-proving-2014/reading/Nieuwenhuis-Rubio.pdf}}</ref>

==參考文獻==
{{refbegin|2}}
* {{cite journal
 |last=[[John Alan Robinson|Robinson]]
 |first=J. Alan
 |title=A Machine-Oriented Logic Based on the Resolution Principle
 |journal=[[Journal of the ACM]]
 |year=1965|volume=12|issue=1|pages=23–41
 |doi=10.1145/321250.321253
}}
* {{cite book
 | last = Leitsch
 | first = Alexander
 | title = The Resolution Calculus
 | publisher = [[Springer Science+Business Media|Springer]]
 | year = 1997
}}
* {{cite book
 | last = Gallier
 | first = Jean H.
 | authorlink = Jean Gallier
 | title = Logic for Computer Science: Foundations of Automatic Theorem Proving
 | publisher = [[Harper & Row]] Publishers
 | year = 1986
 | url = http://www.cis.upenn.edu/~jean/gbooks/logic.html
 | access-date = 2018-08-16
 | archive-date = 2018-08-08
 | archive-url = https://web.archive.org/web/20180808093528/http://www.cis.upenn.edu/~jean/gbooks/logic.html
 | dead-url = no
 }}
* {{cite book
 |last=Lee
 |first=Chin-Liang Chang, Richard Char-Tung
 |title=Symbolic logic and mechanical theorem proving
 |url=https://archive.org/details/symboliclogicmec00chan
 |year=1987|publisher=Academic Press
 |location=San Diego
 |isbn=0-12-170350-9
 |edition=[reprint]
}}
Approaches to '''non-clausal resolution''', i.e. resolution of first-order formulas that need not be in [[clausal normal form]], are presented in:
* {{cite thesis| type=Master's Thesis| author=D. Wilkins| title=QUEST — A Non-Clausal Theorem Proving System| year=1973| publisher=Univ. of Essex, England}}
* {{cite techreport| author=Neil V. Murray| title=A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic| date=Feb 1979| number=2-79| institution=Syracuse Univ.| url=http://surface.syr.edu/cgi/viewcontent.cgi?article=1005&context=eecs_techreports| access-date=2018-08-16| archive-date=2020-06-07| archive-url=https://web.archive.org/web/20200607054416/https://surface.syr.edu/cgi/viewcontent.cgi?article=1005&context=eecs_techreports| dead-url=no}} (Cited from Manna, Waldinger, 1980 as: "A Proof Procedure for Non-Clausal First-Order Logic", 1978)
* {{cite journal| author=[[Zohar Manna]], [[Richard Waldinger]]| title=A Deductive Approach to Program Synthesis| journal=[[ACM Transactions on Programming Languages and Systems]]| date=Jan 1980| volume=2| pages=90–121| doi=10.1145/357084.357090| url=http://www.dtic.mil/get-tr-doc/pdf?AD=ADA065558| access-date=2018-08-16| archive-date=2017-09-27| archive-url=https://web.archive.org/web/20170927052012/http://www.dtic.mil/get-tr-doc/pdf?AD=ADA065558| dead-url=no}} A preprint appearead in Dec 1978 as [http://www.sri.com/sites/default/files/uploads/publications/pdf/725.pdf SRI Technical Note 177] {{Wayback|url=http://www.sri.com/sites/default/files/uploads/publications/pdf/725.pdf |date=20170227140017 }}
* {{cite journal| author=N. V. Murray| title=Completely Non-Clausal Theorem Proving| journal=[[Artificial Intelligence (journal)|Artificial Intelligence]]| year=1982| volume=18| pages=67–85| doi=10.1016/0004-3702(82)90011-x}}
* {{cite journal| author=Schmerl, U.R.| title=Resolution on Formula-Trees| url=https://archive.org/details/sim_acta-informatica_1988-05_25_4/page/425| journal=[[Acta Informatica]]| year=1988| volume=25| pages=425–438| doi=10.1007/bf02737109}} [http://www.zentralblatt-math.org/ioport/en/?id=2297405&type=pdf Summary] {{Wayback|url=http://www.zentralblatt-math.org/ioport/en/?id=2297405&type=pdf |date=20160304192314 }}
{{refend}}

== 外部链接 ==
*[http://mathworld.wolfram.com/ResolutionPrinciple.html Resolution Principle] {{Wayback|url=http://mathworld.wolfram.com/ResolutionPrinciple.html |date=20051124113353 }}
*[http://mathworld.wolfram.com/Resolution.html Resolution] {{Wayback|url=http://mathworld.wolfram.com/Resolution.html |date=20051124105525 }}

[[Category:推理规则]]
[[Category:计算机逻辑]]