逻辑学程序设计与Prolog.pptx

逻辑学程序设计与PrologS的可满足性化简例子：如何提高搜索的效率、限制搜索空间

判断S的可满足性是NP完全问题

一是通过终结无望路径上的搜索

二是制定替代路径上的次序T-消解是指父子句均非重言式式的消解。

T消解的可靠性

T消解的完全性：证明基本上同前。

忽略重言式令A为一个指派，A-消解是指父子句之中至少有一个在A下为假的消解。（如果所有的父子句在A下都为真，那么消解式也为真。而没有在A下失败的子句，就不能期望得到不可解性。）

A-消解的完全性：对于任意的A和S，如果S∈UNSAT，则□∈。

假设我们已经给所有的命题字母编了索引。对于有序消解，我们想通常那样来定义有序消解的闭包
索引号时，只允许{}进行消解；

UNSAT的递归定义：
1）如果□;
2)如果没有命题字母的索引小于出现在S中的p的索引号，，那么;

有序消解的完全性：如果S是不可以满足的，则存在S的一个有序消解反驳。
定义：C的从S出发的线性消解演绎或证明是指满足C=以及下列条件的有序对序列<>,….<>:
（1）以及每个，要么是S中的元素，要么是某个j<i的；
（2）每个(i<=n)都是的消解；
定义：通常我们说C是从S出发线性可演绎的或线性可证的，记为如果存在C从S出发的线性演绎。如果存在C从S出发的线性演绎。Horn子句与Prolog如果S是由Horn子句构成的一个不可满足的集合，那么存在□的一个从S出发线性消解演绎。

我们只需要寻找一个线性序列来证明不可满足性。

在Prolog中，给定目标子句，我们可以要求□的演绎从目标子句出发，并且边子句仅仅从Porlog程序的子句中挑选。定义：令P是程序子句的集合，G是一个目标子句，S=的线性插入消解反驳是指S的由G开始的线性消解反驳，并且该反驳中所有边子句来自P（插入子句）。

定理：令P是程序子句的集合，G是目标子句，如果S=则存在S的一个线性插入消解反驳。

这是Prolog消解证明的一般模式。机器通常把子句存贮为文字的序列，将子句作为序列而不是集合来处理。定理：Prolog中SLD反驳的完全性：如果，那么存在一

如何组织搜索？
SLD树：将所有的SLD推导画成一棵树标签树T。T的根标识为G（目标子句），如果T的任意一个节点标识为G’，则其直接后续由G’与P（程序）中的各种可能的子句选择消解G’最左端的文字是得到的那些消解树进行标识。
例子：第3章基于谓词逻辑的
自动推理与Prolog3.1一阶谓词逻辑P(x1,x2,…,xn)为了表达个体之间的对应关系，我们引入通常数学中函数的概念和记法。例如我们用father(x)表示x的父亲，用sum(x,y)表示数x和y之和，一般地，我们用如下形式：以后我们约定用大写英文字母作为谓词符号,用小写字母f,g,h等表示函数符号,用小写字母x,y,z等作为个体变元符号,用小写字母a,b,c等作为个体常元符号。
我们把“所有”、“一切”、“任一”、“全体”、“凡是”等词统称为全称量词,记为x;把“存在”、“有些”、“至少有一个”、“有的”等词统称为存在量词,记为x。同理,我们可以把命题“存在不是偶数的整数”表示为不同的个体变元,可能有不同的个体域。为了方便和统一起见,我们用谓词表示命题时,一般总取全总个体域,然后再采取使用限定谓词的办法来指出每个个体变元的个体域。具体来讲,有下面两条：
(1)对全称量词,把限定谓词作为蕴含式之前件加入,即x(P(x)→…)。
(2)对存在量词,把限定量词作为一个合取项加入,即x(P(x)∧…)。
这里的P(x)就是限定谓词。我们再举几个例子。例3.1不存在最大的整数,我们可以把它翻译为3.1.2谓词公式
定义1
(1)个体常元和个体变元都是项。
(2)设f是n元函数符号,若t1,t2,…,tn是项,则f(t1,t2,…,tn)是项。
(3)只有有限次使用(1),(2)得到的符号串才是项。定义2设P为n元谓词符号，t1,t2,…,tn为项，则P(t1,t2,…,tn)称为原子谓词公式，简称原子公式或者原子。
从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面我们给出谓词公式的严格定义，即谓词公式的生成规则。定义3
(1)原子公式是谓词公式。
(2)若A,B是谓词公式，则A,A∧B,A∨B,A→B,AB,xA,xA也是谓词公式。
(3)只有有限步应用(1)，(2)生成的公式才是谓词公式。
由项的定义，当t1,t2,…,tn全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以，全体命题公式也都是谓词公式。谓词公式亦称为谓词逻辑中的合适（式）公式，记为Wff。紧接于量词之后被量词作用(即说明)的谓词公式称为该量词的辖域。例如：
(1)xP(x)。
(2)x(H(x)→G(x