版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
第三章 谓词逻辑与归结原理3.1一阶谓词逻辑语法和语义
3.2一阶谓词逻辑演算规则
3.3演绎推理3.4任意合式公式到子句集的转化3.5谓词演算中的归结3.6归结原理与归结反演系统3.7Herbrand定理定义:逻辑是人们思维活动规律的反映和抽象;逻辑亦称为数理逻辑或符号逻辑,主要研究关于推理、证明等模拟人类智能的问题求解理论和方法,是人工智能的重要基础。定义:逻辑是表达人类思维和推理的最精确和成功的方法。其表现方式和人类自然语言非常接近,并且能利用计算机对其进行精确处理。因此,用逻辑作为知识表示工具自然就容易为人们所接受。逻辑可划分为经典逻辑和非经典逻辑两大类,前者包括命题逻辑和一阶谓词逻辑,后者包括模态逻辑、模糊逻辑、时序逻辑、非单调逻辑、多值逻辑等。3.1一阶谓词逻辑语法和语义谓词逻辑语法定义公式的合适形式。谓词逻辑语义定义公式的解释和真值。推理规则定义如何从已知公式推导出新的公式。3.1一阶谓词逻辑语法和语义3.1.1一阶谓词逻辑语法谓词公式的基本组成成份是谓词符号、变量符号、函数符号、常量符号、量词和谓词连接词,并用圆括弧、方括弧、花括弧和逗号隔开,以表示论域内的关系。
(
y){[(
x)P(x,y)
(
z)L(x,f(z))]
(
x)(G(K)
Q(x))}3.1一阶谓词逻辑语法和语义3.1.1一阶谓词逻辑语法常量用来表示特定的事物或概念(个体);变量表示非特定的事物或概念;谓词P(x1,x2,…,xn)用来表达n个实体之间的关系或属性,其中x1,x2,…,xn为个体变量。谓词的取值为T(真)或F(假);函数f(x1,x2,…,xn)实现个体域中n个个体到某一个体的映射,其中x1,x2,…,xn为个体变量。函数没有真假取值。3.1一阶谓词逻辑语法和语义3.1.1一阶谓词逻辑语法不含任何谓词连接词和量词的谓词公式是谓词演算的基本公式,称为原子公式。原子公式WORKMATE(ZHANG,LI),其中ZHANG和LI为常量符号,WORKMATE为谓词符号。3.1一阶谓词逻辑语法和语义3.1.1一阶谓词逻辑语法连接词
(否定、非),
(合取、与),
(析取、非),→(蕴涵、IF…THEN),≡(等价、双条件)量词
(全称量词),表示所有的,
xF(x)
(存在量词),表示存在某一些,
xF(x)通常约定连接词和量词的优先级为:,,最高;
次之;
再次之;→,≡最低。3.1一阶谓词逻辑语法和语义3.1.1一阶谓词逻辑语法利用连接词和量词,可以合成复杂的谓词公式,用来表达复杂的领域知识。用谓词S(x)表示个体x学习好,W(x)表示x工作好;谓词公式S(x)
W(x)表示x不仅学习好而且工作好,
S(y)
W(y)表示y的学习好但工作不好;谓词公式
z(Computer(z)→CPU(z))表示所有的计算机(个体z)都有CPU。3.1一阶谓词逻辑语法和语义3.1.1一阶谓词逻辑语法谓词演算合式公式(WellFormedFormula,WFF)的递归定义如下:
①谓词演算的原子公式是合式公式。 ②若A是合式公式,则
A是合式公式。 ③若A和B是合式公式,则A
B、A
B、A→B、A≡B是
合式公式。 ④若A是合式公式,x是个体变量,则∀x(A)、∃x(A)是
合式公式。
所有合式公式都是有限次应用规则①至规则④得到的。3.1一阶谓词逻辑语法和语义3.1.2世界及解释一阶谓词逻辑可以指称世界中的对象。世界中有无限多的对象,也称为个体。只要定义一个名称,并且有确定的含义,就可以把它当作我们要谈论的这个世界中的一个实际的个体。对象可以是具体的,例如“木块A”、“张三”等;也可以是抽象的,如“数字7”、“所有整数的集合”等;甚至可以是虚构的或者创造的,例如“圣诞老人”、“麒麟”等。3.1一阶谓词逻辑语法和语义3.1.2世界及解释个体上的函数可以有无限多的多元函数,映射n元个体到某个个体。例如:一个函数映射某人到其父亲,或者一个函数映射数字10和2到商数5。个体可以参与任意数目的关系。个体可能会有像“重”、”蓝”等这样的属性,也可能参与到如“比⋯⋯大”、“在⋯⋯之间”等这样的关系中。如果要指明一个n元关系,就要显式地列出所有参与该关系的n元个体。3.1一阶谓词逻辑语法和语义3.1.2世界及解释对谓词公式中的谓词、常量和函数符号赋予具体意义的过程称作谓词公式的解释。设L是一个合式公式,L的解释I由下面4部分组成:为个体变元指定一个论域D;为函数符号指定一个具体的函数;为谓词符号指定一个具体的谓词;为个体常元指定一个具体的个体;3.1一阶谓词逻辑语法和语义3.1.2世界及解释在谓词公式解释I的基础上,为每个自由变元指定一个具体的个体,称为谓词公式解释I上的一个赋值V。谓词公式∀x(M(x)→F(x))∧∃x(H(x)∧F(x))解释I1:论域为全总个体域,M(x):x是人,H(x):x是海豚,F(x):x会走路。3.1一阶谓词逻辑语法和语义3.1.2世界及解释合式表达式需要在一个具体的解释下判断真假谓词公式∀x(M(x)→F(x))∧∃x(H(x)∧F(x))解释I1:论域为全总个体域,M(x):x是人,H(x):x是海豚,F(x):x会走路。在解释I1下得到命题“人都会走路但有的海豚也会走路”,谓词公式在该解释下为真。3.1一阶谓词逻辑语法和语义3.1.3模型及其概念如果一个合式公式在某种解释下为真,则这个解释就满足这个合式公式,该合式公式称为可满足式,或普遍有效的公式。满足合式公式的一个解释就是这个合式公式的模型。任何一个合式公式在所有的解释下都有真值,该合式公式称为永真式。任何一个合式公式在所有的解释下都为假,该合式公式称为永假式。任何没有模型的合式公式是不一致的或不可满足的。如果一个合式公式P在所有能使每一个在集合D中的合式公式都有真值的解释上为真,那么D逻辑涵蕴P(表示为D┝P)。当且仅当在所有的解释下两个合式公式U和V都有相同值(即当且仅当两个合式公式互相逻辑地涵蕴时),它们是等价的,表示为U≡V。3.2一阶谓词逻辑演算规则由于谓词逻辑是命题逻辑的推广,命题逻辑中的基本等价式和推理规则在谓词逻辑仍可沿用。由于谓词逻辑中引入了变量及量词,故增加了一些定理和规则,归纳如下:3.2一阶谓词逻辑演算规则3.2.1等价式
双重否定律:
(
P(x))≡P(x)
摩根定律:
(P(x)
Q(x))≡
P(x)
Q(x)
(P(x)
Q(x))≡
P(x)
Q(x)
逆否律: P(x)→Q(x)≡
Q(x)→
P(x)
分配律: P(x)
(Q(x)
R(x))≡(P(x)
Q(x))
(P(x)
R(x))
P(x)
(Q(x)
R(x))≡(P(x)
Q(x))
(P(x)
R(x))
结合律: (P(x)
Q(x))
R(x)≡P(x)
(Q(x)
R(x)) (P(x)
Q(x))
R(x)≡P(x)
(Q(x)
R(x))3.2一阶谓词逻辑演算规则3.2.1等价式
交换律:
P(x)
Q(x))≡Q(x)
P(x)
P(x)
Q(x))≡Q(x)
P(x)
蕴含等价式: P(x)→Q(x)≡
P(x)
Q(x)
易名规则:
xP(x)
xQ(x)≡
xP(x)
yQ(y)
量词转换律:
xP(x)≡
x
P(x)
Q(x)≡
x
Q(x)
量词交换律:
x
yP(x,y)≡
y
xP(x,y)
x
yP(x,y)≡
y∃xP(x,y)3.2一阶谓词逻辑演算规则3.2.1等价式
量词分配律:
x(P(x)
Q(x))≡
xP(x)
xQ(x)
x(P(x)
Q(x))≡
xP(x)
xQ(x)
x(P→Q(x))≡P→
xQ(x)
x(P→Q(x))≡P→
xQ(x)
量词辖域变换等价式(若Q中不含变量):
xP(x)
Q≡
x(P(x)
Q)
xP(x)
Q≡
x(P(x)
Q)
xP(x)
Q≡
x(P(x)
Q)
xP(x)
Q≡
x(P(x)
Q)3.2一阶谓词逻辑演算规则3.2.1等价式
量词消去及引入规则:
①全称量词消去规则:
xP(x)≡P(y)
②全称量词引入规则: P(y)≡
xP(x)
③存在量词消去规则:
xQ(x)≡Q(c)(c为常量)
④存在量词引入规则: Q(c)≡
xQ(x)
⑤有限域量词消去规则:设有限个体域为D={d1,d2,…,dn},则
xP(x)≡P(d1)
P(d2)
…
P(dn)
xQ(x)≡Q(d1)
Q(d2)
…
Q(dn)3.2一阶谓词逻辑演算规则3.2.2推理规则逻辑推理是基于公理集合进行演绎得出结论的过程,可用于证明公式P1∧P2∧……∧Pn→R是否成立。若使谓词公式P=P1
P2
…
Pn为真的任一解释,都使得另一谓词公式R为真,就说P推出了R,P是R的前提,R是P的逻辑结论,用逻辑符号表示为P┝R(或P→R)。谓词演算中有许多规则,用于从已知公式集合中推出新公式,这些导出的公式称为定理。3.2一阶谓词逻辑演算规则3.2.2推理规则给出定理的推理过程及所使用的推理规则序列就构成了该定理的一个证明。常用的推理规则有:假言推理规则:已知谓词公式C→D及C,则可推出D。前提及结论引入规则:在推理过程中可随时引入前提,并把推理得到的中间结论作为后继推理的前提。替换规则:谓词公式中任一部分公式都可用其等价的公式替换。推理过程即反复使用谓词演算的基本等价式及推理规则,对已知谓词公式进行变换,得到所需逻辑结论的过程。3.3演绎推理基于一组已知为真的事实,利用经典逻辑的推理规则推出结论的过程称为演绎推理。设已知以下事实:
①如果x和y是同班同学,则x的老师也是y的老师。
②张先生是小王的老师。
③小王和小李是同班同学。
求证:张先生是小李的老师。应用演绎推理方法证明定理时,推理过程中得到的中间结论通常呈指数形式递增,容易产生组合爆炸问题。3.3演绎推理为了提高演绎系统的效率,通常对合式公式的形式做出一些限制。常见的限制方式包括:
①设法消去存在量词,使每个公式只剩下隐含的全称量词;
②消去所有的蕴含和等价连接符;
③让所有的非符号只在谓词之前。这样化简之后的合式公式称为与或句。与或句进一步化简,得到子句。3.4合式公式到子句集的转化基于谓词演算规则,任何一个合式公式都可以转化为子句集。其大致过程是:将合式公式转换为前束标准型转换为Skelom标准型转换为合取范式每一个合取项即为一个子句。3.4合式公式到子句集的转化3.4.1Skelom标准型为了方便使用WFF进行定理证明和逻辑推理,需要把WFF变换为便于使用的规范形式,称为WFF范式。典型的范式包括:前束范式,SKOLEM范式。若一个谓词公式P的所有量词均非否定地出现在P的前部,且量词辖域是整个WFF,称P为前束范式或前束标准型。任一WFF都可化为与之等值的前束范式。消去前束范式中的所有存在量词后得到的谓词公式称为SKOLEM范式(或S范式)。S范式与原式不一定等值,但与原式在不可满足性方面等价。3.4合式公式到子句集的转化3.4.1Skelom标准型前束范式的标准形式记为:
F
(Q1x1)…(Qnxn)M(x1,x2,…,xn)
其中(Q1x1)…(Qnxn)为前束,代表各种量词的约束关系,M称为母式,是不包含量词符号的合式公式。例如:
x
yP(x,y)
Q(P(x,y))
x
y
z(
V(P(x,y)
W(z))
3.4合式公式到子句集的转化3.4.1Skelom标准型将合式公式转换为前束标准型的步骤如下:①利用谓词公式的等价关系,消去合式公式中的符号“
”和“
”。②利用双重否定律、德•摩根律、量词转换律,移动否定符号“
”使其作用范围仅限于原子公式。③修改变量名,使得谓词公式中所有量词的约束变量名互不相同,称为变量标准化。④所有量词左移到公式前面,移动过程不可以改变量词前的相对次序。依据以上步骤1-4得到的所有谓词均在公式的最前面,使得所有量词的辖域都延伸到公式尾部,此时的谓词公式即是前束标准型。
3.4合式公式到子句集的转化3.4.1Skelom标准型依据量词消去原则消去或略去前束标准型中的所有量词,得到的谓词公式称为Skelom标准型。由于前束标准型中每个量词的辖域都延伸到公式尾部,那么次序靠右的量词是受那些位次在其前面的量词的约束的。即在某个任意量词辖域范围内的存在量词,与该任意量词有依赖关系。例如,(
y)[(
x)G(x,y)]中x的值与y的值有关。对这种依赖关系,可以定义函数f(y)描述,f(y)将每一个y值映射为一个确定的x值,这样的函数f(y)称为Skelom函数。
3.4合式公式到子句集的转化3.4.1Skelom标准型前束标准型转换为Skelom标准型的步骤如下:
①定义Skelom函数,将谓词公式中存在量词约束的变量用任意常量或任
意变量的函数代替,从而消去存在量词“
”。
②略去全称量词“
”。依据以上步骤1、2得到的谓词公式中不存在量词,此时的谓词公式即是Skelom标准型。需要注意,由于Skelom函数的形式可以有不同定义,所以谓词公式对应的Skelom标准型不唯一。3.4合式公式到子句集的转化3.4.2子句集子句是一些文字的析取,其中,文字是不含任何连接词的谓词公式。只包含一个文字的子句称为单元子句。不含任何文字的子句称为空子句,记作“
”。子句集指由子句构成的集合。基于谓词演算规则,任何一个合式公式都可以转换为子句集3.4合式公式到子句集的转化3.4.2子句集将一个合式公式转换为子句集的基本步骤如下:将合式公式转换为S-范式。把母式化成合取范式。反复使用结合律和分配律,将母式表达成合取范式的标准式(即用
连接的公式)。
略去全称量词。由于母式的变量均受全称量词的约束,可省略掉全称量词(不显式地受全称量词量化)。用子句集表示母式。把母式中每一个合取元称为一个子句,省去合取连接词,这样就可把母式写成集合的形式表示,每个元素就是一个子句。3.4合式公式到子句集的转化3.4.2子句集将一个合式公式转换为子句集的基本步骤如下:5. 子句变量标准化。将子句集合中的变量作分离标准化,即对某些变量重新命名,使任意两个子句不会有相同的变量出现。由于每一个子句都对应一个不同的合取元,变量都由全称量词量化,因而实质上两个子句的变量间不存在任何关系,变量标准化不影响公式的真值。
子句集中所有元素(即子句)的合取式不为真,则称该子句集为不可满足的。3.4合式公式到子句集的转化3.4.2子句集例:将谓词逻辑公式G=
xP(x)→{
y[P(y)→P(f(x,y))]
y[Q(x,y)→P(y)]}变换为子句集。
1.重复运用蕴涵等价式,消去蕴涵词
G=
xP(x)
{
y[
P(y)
P(f(x,y))]
y[~Q(x,y)
P(y)]}2.重复运用摩根律内移否定词~的辖区范围
G=
x
P(x)
{
y[
P(y)
P(f(x,y))]
y
[
Q(x,y)
P(y)]}
=
x
P(x)
{
y[
P(y)
P(f(x,y))]
y[Q(x,y)
P(y)]}3.4合式公式到子句集的转化3.4.2子句集例:将谓词逻辑公式G=
xP(x)→{
y[P(y)→P(f(x,y))]
y[Q(x,y)→P(y)]}变换为子句集。3.变量改名
G=
x
P(x)
{
y[
P(y)
P(f(u,y))]
w[Q(z,w)
P(w)]}
4.移动所有量词到M的前部,移动时不要改变其相对顺序,形成前束范式:
G=
x
y
w
P(x){[
P(y)
P(f(u,y))]
[Q(z,w)
P(w)]}3.4合式公式到子句集的转化3.4.2子句集例:将谓词逻辑公式G=
xP(x)→{
y[P(y)→P(f(x,y))]
y[Q(x,y)→P(y)]}变换为子句集。
5.消去存在量词,把所得的前束范式化为S范式: G=
y
P(a)
{[
P(y)
P(f(u,y))]
[Q(z,g(y))
P(g(y))]},
x=a,w=g(y)为设定的SKOLEM函数。6.将母式M化为合取范式(利用结合律)
y[
P(a)
P(y)
P(f(u,y))]
[
P(a)
Q(z,g(y))]
[
P(a)
P(g(y))]3.4合式公式到子句集的转化3.4.2子句集例:将谓词逻辑公式G=
xP(x)→{
y[P(y)→P(f(x,y))]
y[Q(x,y)→P(y)]}变换为子句集。
7.隐去M前面的量词,得
[
P(a)
P(y)
P(f(u,y))]
[
P(a)
Q(z,g(y))]
[
P(a)
P(g(y))]
8.以逗号替代所有合取符号,得到子句集
P(a)
P(y)
P(f(u,y)),
P(a)
Q(z,g(y)),
P(a)
P(g(y))3.5谓词演算中的归结3.5.1命题公式的归结设C1和C2是子句集中的任意两个字句,如果C1中的文字L1和C2中的文字L2互补,那么从C1和中C2分别消去L1和L2,则两个子句中余下的文字的析取构成一个新子句C12,这个过程称为归结。C12称为C1和C2的归结式,C1和C2称为C12的亲本子句。3.5谓词演算中的归结3.5.1命题公式的归结以下为几种不同情况下的子句归结:
①C1=P,C2=
P,
P和
P是互补文字,C1和C2归结,得到归结式C12=
。
②C1=P
Q
R,C2=
Q
S,
Q和
Q是互补文字,C1和C2归结,得到归结式C12=P
R
S。
③C1=P
Q,C2=
Q
S,C3=
S, Q和
Q是互补文字,C1和C2归结,得到归结式C12=P
S;
S和
S是互补文字,C12和C3归结,得到归结式C123=P。3.5谓词演算中的归结3.5.2置换与合一在谓词逻辑中,由于子句中包含有变元,所以不能直接消去互补文字(L和~L)。需要考虑变量的约束问题,即在应用归结法时,往往要对公式作变量置换和合一等处理,才能得到互补的基本式,然后进行归结。进行置换的目的:为了使用前面的推理规则,一个推理系统必须决定两个表达式是否相同或匹配,两个表达式匹配当且仅当其语法是等价的。3.5谓词演算中的归结3.5.2置换与合一置换是有序对的集合:s={t1/v1,t2/v2,…,tn/vn},其中ti/vi表示将表达式中所有的变量vi都用项ti代替,ti是常量、变量或函数。注意,一个变量不能用含有同一个变量的项来代替。合一就是寻找变量的置换,使两个或多个表达式一致。例如,为使公式
xP(x)与P(A)匹配,可用常量A替换x,从而使两个公式一致。3.5谓词演算中的归结3.5.2置换与合一表达式P[x,f(y),A],应用不同的置换可得到不同的例:
置换的例相应的置换
P[z,f(w),A] s1={z/x,w/y} P[x,f(B),A] s2={B/y} P[g(z),f(B),A] s3={g(z)/x,B/y} P[C,f(B),A] s4={C/x,B/y}第一个例叫做原始文字的初等变式,即置换后只是对变量作了换名。3.5谓词演算中的归结3.5.2置换与合一有时需要对表达式进行多次置换,如用s1、s2依次进行置换即(Es1)s2,这时可以把两个置换合成为一个置换,记为s1s2。合成置换是由两部分组成的:一部分仍是s1的置换对,只是s1中的项被s2作了置换;另一部分是s2中与s1不同的那些变量对。例如:
s1={g(x,y)/z},s2={A/x,B/y,C/w,D/z}s1s2={g(A,B)/z,A/x,B/y,C/w}3.5谓词演算中的归结3.5.2置换与合一这样的合成可使(Es1)s2=E(s1s2),即置换的合成是可以结合的,但容易检验出,一般情况下置换是不可交换的,即s1s2
s2s1。
s2s1={A/x,B/y,C/w,D/z}
s1s23.5谓词演算中的归结3.5.2置换与合一若存在一个置换s使得表达式集{Ei}中每一个元素经置换后的例有:E1s=E2s=E3s=
,则称表达式集{Ei}是可合一的,这个置换s称作{Ei}的合一。例:子句集{P(x,f(y),B),P(x,f(B),B)},对子句集应用置换s={A/x,B/y}得到{P(A,f(B),B)},因而该子句集是可合一的。如果g是谓词公式集{Ei}的一个合一,如果对{Ei}的任意一个合一S都存在一个置换s
,使得S=gs
,则称g为表达式{Ei}的最一般合一mgu(MostGeneralUnifier)。合一g={B/y}为表达式{P(x,f(y),B),P(x,f(B),B)}的最一般合一(s={A/x,B/y},置换s
={A/x})。3.5谓词演算中的归结3.5.2置换与合一求最一般合一的算法:1.令W={F1,F2};//输入2.k=0,Wk=W,gk={};//循环次数,公式集合,置换的初始化3.如果Wk已合一,停止,gk=mgu;//成功退出否则,找不一致集Dk;4.若Dk中存在元素vk和tk,其中vk不出现于tk中,转(5),
否则,不可合一;//失败退出5.令gk+1=
gk•{tk/vk},Wk+1=Wk{tk/vk},//置换合成,公式集合变换6.k=k+1转(3)3.5谓词演算中的归结3.5.3谓词逻辑公式的归结设C1和C2是两个无公共变量的子句,令L1和L2分别是C1和C2中的两个文字。若集合{L1,
L2}存在最一般合一置换
,则子句(C1
-{L1}
)
(C2
-{L2}
)称为C1和C2的二元归结式。L1和L2称为被归结的文字。若子句C中的两个或多个文字构成的集合存在最一般合一置换
,则称C
为C的因子。若C
是单元子句,则称它为C的单元因子。3.5谓词演算中的归结3.5.3谓词逻辑公式的归结归结式C12是其亲本子句C1和C2的逻辑结论,即,如果C1和C2为真则C12为真。
证明:设C1=L
C1',C2=(~L)
C2',通过归结可得到C=C1'
C2'因为C1=L
C1'=C1'
L
~C1'
L; C2=
~L
C2'
L
C2'C1
C2=(~C1'
L)
(L
C2')由假言三段论得到:(~C1'
L)
(L
C2')
(~C1'
C2')而~C1'
C2'
C1'
C2'=C
C1
C2
C
[证毕]3.6归结原理与归结反演系统3.6.1归结原理定理3.3令公式W的子句集为P,则W不可满足当且仅当P是不可满足的。推论子句集S={C1,C2,…,Cn}与子句集S1={C,C1,C2,…,Cn}的不可满足性是等价的,S1中的C是C1和C2的归结式,即S1是对S应用归结得到的子句集。要证明子句集S的不可满足性,只要对S中可归结的子句进行归结并把归结式加入S,然后对新的扩充后的子句集证明其不可满足性。由于空子句是不可满足的,在归结过程中一旦得到空子句,即可证明原子句集S是不可满足的。3.6归结原理与归结反演系统3.6.1归结原理归结原理就是从子句集S出发,应用归结推理规则导出子句集S1
,再从S1出发导出S2
,依次类推,直到某一个子句集Sn出现空子句为止。根据定理3.3的推论,若已知Sn为不可满足的,则可逆向依次推得S必为不可满足的。可见,用归结法证明定理,过程比较简单,只涉及归结推理规则的应用问题,因而便于机器实现。3.6归结原理与归结反演系统3.6.2归结反演系统求解一个问题X,通常意味着在知道一些与问题X相关的事实{P1,P2,…,Pn}的条件下,求证某个结论Q是否成立或者求证某个结论Q在什么条件下成立。因此,求解问题X等价于证明Q是P1,P2,…,Pn的逻辑结论,即证明公式P1
P2
…
Pn
Q永真。则求解问题X等价于证明
P1
P2
…
Pn
Q永真,也等价于证明P1
P2
…
Pn
Q永假。进一步地,等价于证明子句集{P1,P2,…,Pn,
Q}不可满足。3.6归结原理与归结反演系统3.6.2归结反演系统应用归结原理证明定理的过程称为归结反演。谓词逻辑的归结反演是仅有一条推理规则的问题求解方法。要证明P
Q,其中P和Q是谓词公式,先建立合式公式G=P
Q,再将G转化为子句集S,只需证明S是不可满足的即可。归结反演的一般步骤是:
①已知的前提表示为谓词公式P。
②待证明的结论表示为谓词公式Q。
③将谓词公式集{P,
Q}化为子句集S。
④对S中可归结的子句做归结,并将归结式放入S。如此反复,直到S中
出现空子句,则停止归结,此时Q得证。3.6归结原理与归结反演系统3.6.2归结反演系统例:证明“由梯形的对角线形成的内错角是相等的”。谓词定义:设谓词T(x,y,u,v)表示“左上顶点为x,右上顶点为y,左下顶点为u,右下顶点为v”的梯形abcd;谓词P(x,y,u,v)表示“线段xy平行于线段uv”;谓词E(x,y,v,u,v,y)表示“∠xyv=∠uvy”。3.6归结原理与归结反演系统3.6.2归结反演系统例:证明“由梯形的对角线形成的内错角是相等的”。1)依据谓词定义,已知前提表示为T(a,b,c,d),待证结论表示为E(a,b,d,c,d,b)2)根据梯形的定义有公理A1:(
x)(
y)(
u)(
v)[T(x,y,u,v)
P(x,y,u,v)]3)根据平行线的性质有公理A2:(
x)(
y)(
u)(
v)[P(x,y,u,v)
E(x,y,v,u,v,y)]根据归结反演过程,证明“由梯形的对角线形成的内错角是相等的”即是要证明A1∧A2∧T(a,b,c,d)∧
E(a,b,d,c,d,b)是不可满足的。将其化为子句集:S={
T(x,y,u,v)
P(x,y,u,v),
P(x′,y′,u′,v′)
E(x′,y′,v′,u′,v′,y′),T(a,b,c,d),
E(a′,b′,d′,c′,d′,b′)}3.6归结原理与归结反演系统3.6.2归结反演系统例:证明“由梯形的对角线形成的内错角是相等的”。
归结反演树3.6归结原理与归结反演系统3.6.2归结反演系统归结反演过程是“对子句集中的子句进行归结直到产生空子句为止”的一个过程,选择哪两个子句做归结是该过程的一个关键问题。对任意一对可归结的子句都做归结,产生大量无用的或者说对归结得到空子句无用的多余子句,这样不仅导致不必要的空间占用,也消耗过多的计算时间,导致归结过程效率较低。因此,需要研究有效的归结控制控制(搜索)策略,目的是在少做一些归结的条件下仍然可以归结得到空子句,从而提高归结效率。3.6归结原理与归结反演系统3.6.2归结反演系统宽度优先策略,首先生成第1层所有的归结式,然后是第2层所有的归结式,依此类推,直到出现了空子句或者不能再进行归结为止。深度优先策略,首先生成一个第1层的归结式,然后用第1层的归结式和第0层的归结式进行归结得到第2层的归结式,依此类推,直到出现了空子句或者不能再进行归结则回溯到上层子句继续归结。单元子句优先策略,在归结过程中优先选择单元子句参与归结。3.6归结原理与归结反演系统3.6.2归结反演系统支持集策略,每一次归结时,亲本子句中至少有一个是与目标公式否定式有关的子句,即目标公式否定式本身或该否定式有关的后裔。线性输入策略,每一次归结时,亲本子句中至少有一个是原始子句集中的子句。祖先过滤策略,每一次归结时,亲本子句中至少有一个是原始子句集中的子句,或者是另一个子句的祖先。祖先过滤策略是完备的,是对线性输入策略的改进。3.6归结原理与归结反演系统3.6.2归结反演系统归结反演不仅可以用于定理证明,还可以用来求取问题的答案,其思想与定理证明类似。基本方法有两个:1)目标公式Q(x)的否定形式
Q(x)与目标公式否定的否定
(
Q(x))析取,构成重言式
Q(x)
Q(x),将新构成的重言式作为一个子句加入到子句集中进行归结;2)定义答案谓词ANS(x),目标公式Q(x)的否定形式
Q(x)与ANS(x)析取得到一个新的子句
Q(x)
ANS(x),将新的子句加入到子句集中进行归结。注意归结的过程中,首先对包含目标否定的字句进行归结。3.6归结原理与归结反演系统3.6.2归结反演系统例:如果x和y是同班同学,则x的老师也是y也老师;ZHANG和WANG是同班同学;LI是ZHANG的老师。WANG的老师是谁?谓词定义:设谓词C(x,y)表示“x和y是同班同学”;谓词T(x,z)表示“x的老师是z”。依据谓词定义,已知前提包括:(
x)(
y)(
z)[(C(x,y)∧T(x,z))
T(y,z)],C(ZHANG,WANG),T(ZHANG,LI);目标公式的否定为:
uT(WANG,u)。3.6归结原理与归结反演系统3.6.2归结反演系统采用重言式的方式,得到子句集{
C(x,y)
T(x,z)
T(y,z),C(ZHANG,WANG),T(ZHANG,LI),
T(WANG,u)
T(WANG,u)},修改证明树如下:3.6归结原理与归结反演系统3.6.2归结反演系统采用答案谓词的方式,得到子句集{
C(x,y)
T(x,z)
T(y,z),C(ZHANG,WANG),T(ZHANG,LI),
T(WANG,u)
ANS(u)},修改证明树如下:3.7Herbrand定理Herbrand定理将对永真性的证明转化成对不可满足性的证明,是归结原理的理论基础,是归结原理完备性的保证。同时,归结原理是Herbrand定理的具体实现。3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释设S是一个子句集,S定义在论域D上,H0是S中子句所包含的全体常量集。若S中所有子句均不包含常量,则选择任一常量a,并令H0={a}。Hi=Hi-1∪{fm(t1,…,tm)|m≥1,fm为S中出现的秩为m的函数,t1,…,tm∈Hi-1},H∞=H0∪H1∪H2∪…。Hi称为S的i阶常量集。H∞称为S的Herbrand论域。H∞的元素称为基项。3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释子句集S={P(x),Q(f(a))
R(g(b))},S的Herbrand论域如下: H0={a,b} H1={a,b,f(a),f(b),g(a),g(b)} H2={a,b,f(a),f(b),g(a),g(b),f(f(a)),f(f(b)),f(g(a)),f(g(b)),
g(f(a)),g(f(b)),g(g(a)),g(g(b)} H3=……… H∞=H0∪H1∪H2∪…3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释设S是一个子句集,H∞是S的Herbrand论域,则S的Herbrand基定义为={Pn(t1,…,tn)|n≥1,t1,…,tn∈H∞,Pn为S中出现的秩为n的谓词}。
也称为原子集。3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释子句集S={P(x),Q(f(a))
R(g(b))},S的Herbrand基如下: ={P(a),Q(a),R(a),P(b),Q(b),R(b),P(f(a)),Q(f(a)),R(f(a)),P(f(b)),Q(f(b)),R(f(b)),P(g(a)),Q(g(a)),R(g(a)),P(g(b)),Q(g(b)),R(g(b)),P(f(f(a))),Q(f(f(a))),R(f(f(a))),P(f(f(b))),Q(f(f(b))),R(f(f(b))),P(f(g(a))),Q(f(g(a))),R(f(g(a))),P(f(g(b))),Q(f(g(b))),R(f(g(b))),P(g(f(a))),Q(g(f(a))),R(g(f(a))),P(g(f(b))),Q(g(f(b))),R(g(f(b))),P(g(g(a))),Q(g(g(a))),R(g(g(a))),P(g(g(b)),Q(g(g(b)),R(g(g(b)),…}3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释子句集的Herbrand解释由下列几部分组成:
①
S的Herbrand论域H∞。
②S的每个常量c对应H∞中的同一个c。
③S的每个变量x都在H∞中取值。
④S中每个秩为m的函数fm对应一个映射H∞×H∞×…×H∞
H∞(其中,
左边有m个H∞),使得任一组基项(t1,…,tm)的映射即是基项fm(t1,…,tm)。
⑤S中每个秩为n的谓词Pn(t1,…,tn)对应一个映射H∞×H∞×…×H∞
(T,
F)(左边有n个H∞)。其中谓词Pn代表的映射,也是从到(T,F)的一
个映射。3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释
3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释子句集S={P(x),Q(f(a))
R(g(b))}设有常量a的谓词均取值为假,有常量b的谓词均取值为真,则HI为S的Herbrand解释: HI={P(b),Q(b),R(b),P(f(b)),Q(f(b)),R(f(b)),P(g(b)),Q(g(b)),R(g(b)),
P(f(f(b))),Q(f(f(b))),R(f(f(b))),P(f(g(b))),Q(f(g(b))),R(f(g(b))),P(g(f(b))),
Q(g(f(b))),R(g(f(b))),P(g(g(b)),Q(g(g(b)),R(g(g(b)),…}
3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释定理3.4若子句集S对所有H解释都是不可满足的,则子句集对S对任何解释都是不可满足的。需要证明:如果存在一个解释I能够满足子句集S,那么可以找到一个相应的H解释HI,且HI满足子句集S。问题是如何找到HI?根据H解释的定义,只要确定映射m即可以确定HI。可以令中
的谓词Pn(t1,…,tn)取真值,当且仅当它在解释I中取真值,
则由于I使子句集S得到满足,确定了映射后m的H解释HI也使
S得到满足。3.7Herbrand定理3.7.1Herbrand论域与Herbrand解释定理3.4将证明子句集S不可满足的问题缩小为证明S在所有H解释下不可满足,但H解释也有很多。如果子句集S的H基有n个元素,则S有2n种不同解释。因此,需要有适当的方法来搜索这些H解释,以便判断S是否可满足。最常应用的方法是语义树方法。3.7Herbrand定理3.7.2语义树语义树的构建方法为,将子句集S的H基中的元素逐层添加到一颗二叉树,并将元素的“是”与“非”分别标记在两侧的分支上。子句集S={
P(f(x)),Q(f(y)),P(z)
Q(z)}对应的语义树3.7.2语义树对相应于子句集S的一株语义树,如果在从根节点到任一叶结点的路径都包含了H∞中的每个原子或其负原子,则该语义树是完备的,称为S的完全语义树。在构建语义树的过程中,如果某个分支延伸到节点N时,I(N)已使S的某一子句的某一基例为假,那么这个分支没有必要再延伸,节点N称为失败节点。如果S的完全语义树的每个分支上都有一个失败节点,则称它是一棵封闭语义树。3.7Herbrand定理3.7.2语义树子句集S={
P(f(x)),Q(f(y)),P(z)
Q(z)}的封闭树3.7Herbrand定理3.7Herbrand定理3.7.3Herbrand定理与归结法的完备性定理3.5(Herbrand定理Ⅰ)子句集S是不可满足的,当且仅当S对应的每株完全语义树均是封闭语义树。定理3.6(Herbrand定理Ⅱ)子句集S是不可满足的,当且仅当存在一个有限的不可满足的基子句集S′,其中的每一子句都是S中某个子句的基例。Herbrand定理II表明,要证明一个子句集的不可满足性,只要证明该子句集的一个有限的基子句集不可满足就可以了。3.7Herbrand定理3.7.3Herbrand定理与归结法的完备性子句集S={P(x),Q(f(y)),
P(a)
P(b)}的H论域和H基都是无限的,但这不妨碍对于S的不可满足性的证明,因为存在一个有限的基子句集{P(a),P(b),
P(a)
P(b)}是不可满足的。3.7Herbrand定理3.7.3Herbrand定理与归结法的完备性通过建立H域、语义树,在无限不可数的个体域上的不可满足问题转换为可数有序域上的问题问题求解,但仍然存在基子句集元素的数量随着子句集元素数量呈指数增长的问题。因此,Herbrand定理在20世纪30年代被提出后并没有直接得到应用,直到1956年Robinson提出归结原理,才使得Herbrand定理有了用武之地。3.7Herbrand定理3.7.3Herbrand定理与归结法的完备性对一个给定的定理,如果定理成立,使用归结法是否一定能证明这个定理?对一个公理体系,已知定理数量,使用归结法推导的定理数量是否与已知的定理数量一致?回答以上两个问题,需要讨论归结法的完备性。3.7Herbrand定理3.7.3Herbrand定理与归结法的完备性归结法的归结过程是语义树的倒塌过程,以子句集S={P,
P
R,
P
R}的归结为例。归结过程
①P
②
P
R
③
P
R
④
P
归结②与③,对应语义树T1
⑤󠆙󠆙
归结①与④,对应语义树T23.7Herbrand定理3.7.3Herbrand定理与归结法的完备性归结法的归结过程是语义树的倒塌过程,以子句集S={P,
P
R,
P
R}的归结为例。S的封闭语义树及语义树倒塌过程3.7Herbrand定理3.7.3Herbrand定理与归结法的完备性上例说明子句集的归结过程和子句集的语义树的倒塌过程是相互对应的,对语义树的两个失败节点对应的两个字句进行归结,归结式并入子句集会使得语义树倒塌,重复这个过程直到语义树仅由根节点组成为止。根据Herbrand定理I,不可满足的子句集S一定有对应的封闭语义树,经过对应于归结的倒塌过程,一定可以使根节点成为失败节点,即一定可以得到空子句。因此,对不可满足的子句集S,其不可满足性必然可以通过归结法得以证明,即归结法是完备的。现实世界中由于客观上存在的随机性、模糊性,反映到知识以及由观察所得到的证据上来,就分别形成了不确定性的知识及不确定性的证据。因而还必须对不确定性知识的表示及推理进行研究。这就是将要讨论的不确定性推理。下面首先讨论不确定性的表示与量化,然后着重介绍基于概率论的有关理论发展起来的不确定性推理方法,主要介绍可信度方法、证据理论,最后介绍目前在专家系统、信息处理、自动控制等领域广泛应用的依据模糊理论发展起来的模糊推理方法。第四章不确定性推理推理:从已知事实(证据)出发,通过运用相关知识逐步推出结论或者证明某个假设成立或不成立的思维过程。不确定性推理:从不确定性的初始证据出发,通过运用不确定性的知识,最终推出具有一定程度的不确定性但却是合理或者近乎合理的结论的思维过程。第四章不确定性推理第四章不确定性推理4.1不确定性的表示与量化4.2概率推理主要内容4.3模糊推理4.1不确定性的表示与量化4.1.1不确定性的表示4.1.2不确定性的量化874.1不确定性的表示与量化1.不确定性的表示(1)知识不确定性的表示(2)证据不确定性的表示——证据的动态强度88在专家系统中知识的不确定性一般是由领域专家给出的,通常是一个数值——知识的静态强度
用户在求解问题时提供的初始证据。在推理中用前面推出的结论作为当前推理的证据。4.1不确定性的表示与量化892.不确定性的表示(1)知识不确定性的表示
静态强度可以是相应知识在应用中成功的概率,也可以是该知识的可信程度或其他,其值的大小范围因其意义与使用方法的不同而不同。其中表示事件成立的可能性。例如,(这场球赛中国队获胜,0.5),其中0.5表示上述命题“这场球赛中国队获胜”的信度,即表示“这场球赛中国队获胜”这个命题为真的可能性为0.5。4.1不确定性的表示与量化902.不确定性的表示(1)证据不确定性的表示对于初始证据,其动态强度值通常由用户给出;对于由前序推理所得的结论作为当前推理的证据,其动态强度值由推理中不确定性的传递算法通过计算得到。其中表示规则在前提为真的情形下结论为真的程度。例如,“如果咳嗽发烧,则患了新冠肺炎(0.8)。”这里的0.8就是对应规则结论的信度。它们代替了原命题中的“很可能”和“大概”,可视为规则前提与结论之间的一种关系强度。4.1不确定性的表示与量化2.不确定性的量化
91①
能充分表达相应知识及证据不确定性的程度。②度量范围的指定便于领域专家及用户对不确定性的估计。③
便于对不确定性的传递进行计算,而且对结论算出的不确定性量度不能超出量度规定的范围。④度量的确定应当是直观的,同时应有相应的理论依据。
规则的不确定性量化证据的不确定性量化其中,表示由前提条件得到结论的确定性因子,表示由前提条件得到结论的信任增加度量,表示由前提条件得到结论的不信任增加度量。4.1不确定性的表示与量化2.不确定性的量化(1)规则的不确定性量化引入确定性因子作为规则的不确定性量化。
924.1不确定性的表示与量化实际使用时,初始证据的值经常由领域专家根据经验提供,其他证据的通过规则进行推理计算得到。4.1不确定性的表示与量化2.不确定性的量化(2)证据的不确定性量化为了描述这种不确定性的程度,引入了证据的可信度。证据的可信度用来表示,为了计算方便,规定:
944.1.2不确定性的量化
组合证据不确定性的算法:最大最小方法C(E1ANDE2)=min{C(E1),C(E2)}C(E1ORE2)=max{C(E1),C(E2)}概率方法C(E1ANDE2)=C(E1)C(E2)
C(E1ORE2)=C(E1)+C(E2)-C(E1)C(E2)有界方法C(E1ANDE2)=max{0,C(E1)+C(E2)-1}
C(E1ORE2)=min{1,
C(E1)+C(E2)}954.2概率推理4.2.1概率理论基础4.2.2Bayes网络4.2.3基于Bayes网络的概率推理4.2.4证据理论(D-Stheory)964.2概率推理4.2.1概率理论基础
4.2.2Bayes网络4.2.3基于Bayes网络的概率推理4.2.4证据理论(D-Stheory)974.2.1概率方法概率论:研究随机现象中数量规律的一门学科。随机现象:在相同的条件下重复进行某种实验,所得实验结果不一定完全相同且不可预知的现象。随机事件A的概率P(A):A发生的可能性大小,即事件A的确定性程度。条件概率、Bayes定理可得出一个事件发生的条件下另一个事件的概率,即基于产生式规则的不确定性推理。98条件概率设与是某个随机实验中的两个事件,如果在事件发生的条件下,考虑事件发生的概率,就称它为事件的条件概率。条件概率的定义:设与为两事件且,则称为在事件已发生的条件下,事件发生的条件概率。Bayes定理设,,,…,为一些事件,,,,…,互不相交,,,且,则对于有4.2.1概率理论基础经典概率方法逆概率方法101经典概率方法
产生式规则:
E:前提条件,:结论:在证据出现的条件下,结论成立的确定性程度。102
复合条件:
:在证据出现时结论的确定程度。IFETHENHiE=E1ANDE2AND…ANDEm逆概率方法1.逆概率方法的基本思想:
103
Bayes定理:逆概率原概率
例如::咳嗽,:支气管炎,条件概率:统计咳嗽的人中有多少是患支气管炎的。逆概率:统计患支气管炎的人中有多少人是咳嗽的。
逆概率方法2.单个证据的情况产生式规则:
Bayes公式:104结论的先验概率结论成立时前提条件所对应的证据出现的条件概率
IFETHENHi的的后验概率逆概率方法例1
:结论,:证据。已知:求:105同理可得:解:P(H2∣E)=0.26,
P(H3∣E)=0.43P(H1∣E),P(H2∣E),P(H3∣E)?逆概率方法
多个证据,多个结论,
且每个证据都以一定程度支持结论。
扩充后的公式:1063.多个证据的情况∑1212121)()︳()︳()︳()()︳()︳()︳()︳(njjjmjjiimiimiHPHEPHEPHEPHPHEPHEPHEPEEEHP==LLL
例2
已知:
107逆概率方法
求:P(H1∣E1E2),P(H2∣E1E2),P(H3∣E1E2)?。逆概率方法108解:同理可得:逆概率方法优点:较强的理论背景和良好的数学特征,当证据及结论都彼此独立时计算的复杂度比较低。缺点:要求给出结论的先验概率及证据的条件概率。1094.逆概率方法的优缺点4.2概率推理4.2.1概率理论基础4.2.2Bayes网络4.2.3基于Bayes网络的概率推理4.2.4证据理论(D-Stheory)1104.2.2Bayes网络Bayes网络是一种帮助人们将概率统计应用于复杂领域、进行不确定性推理和数值分析的工具。▶Bayes网络是一种系统地描述随机变量之间关系的语言。▶构造Bayes网络的主要目的是进行概率推理,即计算一些事件发生的概率。▶Bayes网络把联合概率分解成一系列简单模块,从而降低难度▶Bayes网络是概率论与图论结合的产物,一方面用图论的语言直观揭示问题的结构,另一方面按概率论的原则对问题结构加以利用。▶许多经典多元概率模型都是Bayes网络的特例:隐马尔科夫模型、卡尔曼滤波器等。▶Bayes网络学习:从数据出发获得Bayes网络的过程。
▶Bayes网络是一个有向无环图,其中节点代表随机变量,节点间的边代表变量之间的直接依赖关系。每个节点都附有一个概率分布,根节点X的是它的边缘分布P(X),而非根节点X所附的是条件概率分布。
4.2.2Bayes网络▶确定建立网络模型所需的变量及其解释。即,确定模型的目标,即确定问题相关的解释;确定与问题有关的可能观测值,并确定其中值得建立模型的子集;将这些观测值组织成互不相容的而且穷尽所有状态的变量。但是这样做的结果不是惟一的,而且没有通用的解决方案,不过可以从决策分析和统计学得到一些指导原则。▶建立一个表示条件独立的有向无环图。从原理上说,如何从个变量中找出适合条件独立关系的顺序,是一个组合爆炸问题,即要比较种变量顺序。但是,在现实问题中通常可以确定变量之间的因果关系,而且因果关系一般都对应于条件独立的断言。因此,可以从原因变量到结果变量画一个带箭头的弧来直观表示变量之间的因果关系。Bayes网络的构造
▶指派局部概率分布。其中,表示变量的父结点集。在离散的情形,需要为每一个变量的父结点集的各个状态指派一个概率分布。以上各步可能需要交叉并反复进行,不是一次简单的顺序进行就可以完成。Bayes网络的构造
Bayes网络是一种以随机变量为结点
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 职业卫生技术服务专业技术人员考试(职业卫生评价)例题及答案(陕西省汉中市2026年)
- 预防接种测试题及答案
- 新疆伊犁哈萨克自治州部分学校2025-2026学年高一下学期期末考试历史试题(文字版含答案)
- 口腔预防医学测试试题库与答案
- 河北省廊坊市高职单招2026年综合素质自考预测试题(含答案)
- 非煤矿山露天矿山双控双重预防机制建设规范培训试题及答案
- 传播职业技术学院单招职业适应性测试题库及答案
- 2026预防艾滋病知识竞赛试题及答案
- 2026年天津职业大学单招职业技能考试题库及答案
- 2026年厦门工学院单招职业适应性测试题库及答案
- 应急第一响应人培训课件
- 印刷企业毕业论文
- GD2016《2016典管》火力发电厂汽水管道零件及部件典型设计(取替GD2000)-401-500
- 医院安全生产内部举报奖励制度
- 员工反行贿协议书
- 2025江西新余市国有资产经营有限责任公司及其下属子公司招聘3人备考题库带答案详解(完整版)
- 公司法人授权委托书范本模板
- 2025中华护理学会团体标准-成人患者医用粘胶相关性皮肤损伤的预防及护理
- 2025四川成都诸葛资本投资有限责任公司招聘高级投资经理等岗位5人笔试历年典型考点题库附带答案详解试卷2套
- 知识产权运营岗位面试题及准备
- 心血管介入围手术期护理查房
评论
0/150
提交评论