1) resolution principle
归结原理
1.
Research on extensible markup language problem solving based on resolution principle;
基于归结原理的可扩展标识语言问题求解
2.
The Exploration of Problem Solving based on Resolution Principle;
用归结原理进行问题求解的探索
3.
It discusses carefully the basic concepts and inference rule of the resolution principle.
对归结原理的基本概念与推理规则进行了讨论 ,并在此基础上通过实例探讨了归结推理方法在数学定理证明中的应用 。
2) α-resolution Principle
α-归结原理
1.
α-resolution Principle with Generalized Quantifier Based on First-order Lattice-valued Logic LF(X);
格值一阶逻辑系统LF(X)中带广义量词的α-归结原理
3) magnifying or reducing resolution principle
放缩归结原理
1.
In this paper,magnifying or reducing principle and magnifying or reducing resolution principle of lattice-valued propositional logic L9P(X) are given.
给出了格值命题逻辑系统L9P(X)上的放缩原理和放缩归结原理,基于放缩归结原理,给出了一种判断L9P(X)上子句集S为M-可满足的自动推理算法(这里M为L9上的中界元),并证明了其可靠性和完备性。
4) structural induction principle
结构归纳法原理
5) II-α-hyper resolution principle
II-α-超归结原理
1.
In order to improve the efficiency of resolution automated reasoning algorithm in lattice-valued propositional logic, II-α-hyper resolution principle is proposed based onα- resolution principle of lattice-valued propositional logic LP(X).
针对格值命题逻辑中归结自动推理算法的效率问题,在格值命题逻辑系统中的α-归结原理基础上,提出了格值命题逻辑系统LP(X)上的II-α-超归结原理,并证明了其可靠性和完备性。
6) ending principle
归结原则
1.
So,the author points out some shortcomings on solving the limit of duality function and how to solve the problem by means of the ending principle.
为此,作者特指出某些书中求二元函数极限易于出现的问题及应用海涅归结原则如何求解。
补充资料：归结原理
将普通形式逻辑中充分条件的假言联锁推理形式符号化，并向一阶谓词逻辑推广的一种推理法则，又称归结法则、分解法则、消解法则。
基本思想 从应用的角度出发，可以从充分条件的假言联锁推理、命题逻辑的归结原理，一阶谓词逻辑的归结原理等三个方面来分析归结原理的基本思想。
充分条件的假言联锁推理 是前提和结论全部由充分条件假言判断构成的一种推理形式。下面是普通形式逻辑中在引入蕴涵连接词"→"（代表如果......则......的逻辑关系）后的推理图式：
横线上、下方的逻辑公式分别与推理的前提和结论相对应。
由于P→Q (如果P 则Q)和（非P或Q）这两个公式逻辑等价，即（P→Q）呏（塡P∨Q）,同理有（Q→R）呏（塡Q∨R）,（P→R）呏（塡P∨R）。用这些逻辑等价关系的右式分别替换其中的蕴涵公式，即得命题逻辑中使用归结法则的推理图式：
命题逻辑的归结原理 在命题逻辑归结原理的推理图式中，P、Q和R称为原子公式(简称原子),即不使用逻辑连接词的简单命题形式。原子和原子的否定式统称句元，例如P与塡P、Q与塡Q、R与塡R即是三对互补句元。子句就是将不同句元用析取词∨（或）连接而成的析取式。应用归结法则进行推理时，所有判断都写成子句的形式，这不论对命题逻辑还是对一阶谓词逻辑都不例外。
在命题逻辑中，原子被看成一个内部结构不予分析的逻辑基元，代表简单的命题形式。单凭普通形式逻辑中充分条件的假言联锁推理的符号化，只能直接演变为命题逻辑的归结原理。命题逻辑的归结原理或归结法则可归纳如下：对任意两个子句H1和H2，如果H1和H2中各自包含一个互补的句元L1和L2（例如上述图式中的Q和塡Q），则可以删去L1和L2，并将原来的子句H1与H2归结为删去互补句元后两子句余下部分的析取式C。C也以子句形式出现，称为原来两子句（常称为亲子句）的一个归结式例如图式中塡P∨R即为塡P∨Q与塡Q∨R两子句的一个归结式。归结原理或归结法则即因此得名。
一阶谓词逻辑的归结原理 一阶谓词逻辑中，原子是由谓词和项组成的，因而在句元和子句中就有个体变元出现。由于存在量词能用斯科林变换消去，可以认为句元和子句中的个体变元只受全称量词约束 (见逻辑表示)。两个子句H1与H2的归结式可分四种情形:①子句H1与H2的归结式;②子句H 1与子句H2的因子句H2′的二元归结式；③子句H 1的因子句H1′与子句H2的二元归结式；④子句H1、H2各自的因子句H1′与H2′的二元归结式。求子句的因子句和求两子句归结式时,都必须用合一算法求出最普遍合一替换mgu（most general unifier）,或称最广通代。这是在一阶谓词逻辑中应用归结法则的关键技术，最普遍合一替换是在一个表达式集合E={E1,...，Ek}中,用一组项（t1,...,tk）替换一组互异个体变元(x1,...,xk),使替换后的各表达式相等(称为合一)的最简替换。①求子句因子句时的最普遍合一替换：例如子句H1＝P(x)∨P(f(y))∨塡Q(x) 的因子句H1′＝P(f(y))∨塡Q(f(y))，mgu={f(y)/x}。②求两子句（包括子句之一或两子句都有因子句的情形）的二元归结式时的最普遍合一替换:例如子句H 2=塡P(f(g(a))∨R(b),则H2与上例H1的因子句H1′的二元归结式C =塡Q(f(g(a))∨R(b),mgu={g(a)/y}。
应用方法 应用归结原理证明定理或求解问题时采用反证法，即先假设与结论相反的命题是成立的，然后根据前提和否定结论的假设（都以子句形式出现），求出一系列中间结论（以归结式的形式出现），如果最后得到两个相互矛盾的命题（以互补句元形式出现的一对单句元子句），即表明与结论相反的假设不能成立，因而原结论的正确性得证，此时归结式是空子句□。可以从理论上证明一阶谓词逻辑的归结原理是完备的，即一个子句集 S(前提和结论否定式合取形成的全体子句)不可满足的充要条件是从子句集S 中能推导出空子句□。
实施步骤 应用归结法则的具体步骤是：①将定理或问题用逻辑形式表示。②消去存在量词，使公式中出现的所有个体变元只受全称量词约束。③构造子句集，包括将所有前提表示为子句形式；将结论否定也表示为子句形式。④证明子句集S的不可满足性,即应用归结法则和合一算法，反复推求两子句的归结式（对命题逻辑情形无需采用合一算法）,直到最终推导出空子句□,即表明定理得证或问题有解。这个推理过程由计算机自动进行。
应用举例 表说明归结法则在自动演绎中的应用。
根据归结原理进行推理时只需要一条推理规则，即求两子句归结式的归结法则，所以使用简便，容易在计算机上实现。后来发现对于复杂的推理问题，中间归结式的产生会陷入盲目状态，缺乏可以明确遵循的搜索策略,使推理效率大为降低。为此又提出一些改进方案,如语义归结、锁归结、线性归结等，此外还对广义归结进行了研究。
参考书目
中国人民大学哲学系逻辑教研室编:《形式逻辑》,中国人民大学出版社，北京，1984。Ching-Liang Chang and Richard Char-Tung Lee， Symbolic Logic and Mechanical Theorem Proving，Academic Press,Inc.,New York,1973.
基本思想 从应用的角度出发，可以从充分条件的假言联锁推理、命题逻辑的归结原理，一阶谓词逻辑的归结原理等三个方面来分析归结原理的基本思想。
充分条件的假言联锁推理 是前提和结论全部由充分条件假言判断构成的一种推理形式。下面是普通形式逻辑中在引入蕴涵连接词"→"（代表如果......则......的逻辑关系）后的推理图式：
横线上、下方的逻辑公式分别与推理的前提和结论相对应。
由于P→Q (如果P 则Q)和（非P或Q）这两个公式逻辑等价，即（P→Q）呏（塡P∨Q）,同理有（Q→R）呏（塡Q∨R）,（P→R）呏（塡P∨R）。用这些逻辑等价关系的右式分别替换其中的蕴涵公式，即得命题逻辑中使用归结法则的推理图式：
命题逻辑的归结原理 在命题逻辑归结原理的推理图式中，P、Q和R称为原子公式(简称原子),即不使用逻辑连接词的简单命题形式。原子和原子的否定式统称句元，例如P与塡P、Q与塡Q、R与塡R即是三对互补句元。子句就是将不同句元用析取词∨（或）连接而成的析取式。应用归结法则进行推理时，所有判断都写成子句的形式，这不论对命题逻辑还是对一阶谓词逻辑都不例外。
在命题逻辑中，原子被看成一个内部结构不予分析的逻辑基元，代表简单的命题形式。单凭普通形式逻辑中充分条件的假言联锁推理的符号化，只能直接演变为命题逻辑的归结原理。命题逻辑的归结原理或归结法则可归纳如下：对任意两个子句H1和H2，如果H1和H2中各自包含一个互补的句元L1和L2（例如上述图式中的Q和塡Q），则可以删去L1和L2，并将原来的子句H1与H2归结为删去互补句元后两子句余下部分的析取式C。C也以子句形式出现，称为原来两子句（常称为亲子句）的一个归结式例如图式中塡P∨R即为塡P∨Q与塡Q∨R两子句的一个归结式。归结原理或归结法则即因此得名。
一阶谓词逻辑的归结原理 一阶谓词逻辑中，原子是由谓词和项组成的，因而在句元和子句中就有个体变元出现。由于存在量词能用斯科林变换消去，可以认为句元和子句中的个体变元只受全称量词约束 (见逻辑表示)。两个子句H1与H2的归结式可分四种情形:①子句H1与H2的归结式;②子句H 1与子句H2的因子句H2′的二元归结式；③子句H 1的因子句H1′与子句H2的二元归结式；④子句H1、H2各自的因子句H1′与H2′的二元归结式。求子句的因子句和求两子句归结式时,都必须用合一算法求出最普遍合一替换mgu（most general unifier）,或称最广通代。这是在一阶谓词逻辑中应用归结法则的关键技术，最普遍合一替换是在一个表达式集合E={E1,...，Ek}中,用一组项（t1,...,tk）替换一组互异个体变元(x1,...,xk),使替换后的各表达式相等(称为合一)的最简替换。①求子句因子句时的最普遍合一替换：例如子句H1＝P(x)∨P(f(y))∨塡Q(x) 的因子句H1′＝P(f(y))∨塡Q(f(y))，mgu={f(y)/x}。②求两子句（包括子句之一或两子句都有因子句的情形）的二元归结式时的最普遍合一替换:例如子句H 2=塡P(f(g(a))∨R(b),则H2与上例H1的因子句H1′的二元归结式C =塡Q(f(g(a))∨R(b),mgu={g(a)/y}。
应用方法 应用归结原理证明定理或求解问题时采用反证法，即先假设与结论相反的命题是成立的，然后根据前提和否定结论的假设（都以子句形式出现），求出一系列中间结论（以归结式的形式出现），如果最后得到两个相互矛盾的命题（以互补句元形式出现的一对单句元子句），即表明与结论相反的假设不能成立，因而原结论的正确性得证，此时归结式是空子句□。可以从理论上证明一阶谓词逻辑的归结原理是完备的，即一个子句集 S(前提和结论否定式合取形成的全体子句)不可满足的充要条件是从子句集S 中能推导出空子句□。
实施步骤 应用归结法则的具体步骤是：①将定理或问题用逻辑形式表示。②消去存在量词，使公式中出现的所有个体变元只受全称量词约束。③构造子句集，包括将所有前提表示为子句形式；将结论否定也表示为子句形式。④证明子句集S的不可满足性,即应用归结法则和合一算法，反复推求两子句的归结式（对命题逻辑情形无需采用合一算法）,直到最终推导出空子句□,即表明定理得证或问题有解。这个推理过程由计算机自动进行。
应用举例 表说明归结法则在自动演绎中的应用。
根据归结原理进行推理时只需要一条推理规则，即求两子句归结式的归结法则，所以使用简便，容易在计算机上实现。后来发现对于复杂的推理问题，中间归结式的产生会陷入盲目状态，缺乏可以明确遵循的搜索策略,使推理效率大为降低。为此又提出一些改进方案,如语义归结、锁归结、线性归结等，此外还对广义归结进行了研究。
参考书目
中国人民大学哲学系逻辑教研室编:《形式逻辑》,中国人民大学出版社，北京，1984。Ching-Liang Chang and Richard Char-Tung Lee， Symbolic Logic and Mechanical Theorem Proving，Academic Press,Inc.,New York,1973.
说明：补充资料仅用于学习参考，请勿用于其它任何用途。
参考词条