`
somefuture
  • 浏览: 1090056 次
  • 性别: Icon_minigender_1
  • 来自: 上海
社区版块
存档分类
最新评论

合取范式的可满足性判定算法和谓词逻辑不可判定性

 
阅读更多

作为本系列的最后一篇文章,我们来看被广为研究的SAT问题。

SAT问题是第一个被证明为NP问题的判定问题。更多信息可以去百度或者维基一下。

 

前面我们看到了Horn公式可满足性的判定算法,现在把它推广到任意公式Φ。首先将公式变换成具有下面语法的等值公式:φ ::= p | (¬φ) | (φ ∧ φ)。变换方法如下(已被证明变换后是等价的):

 在结果T(φ)的语法树中要公共子公式共享,这样将语法树变成一个有向无回路(环)图(DAG)。

例如,φ = p∧ ¬(q ∨¬p),变换后T(φ)=p ∧¬¬(¬q ∧¬¬p)。它们语法树分别是:

 看明白怎么就是“分享子公式”了吧。

对于变换后的语法树进行从上到下的标记,根部标记T,如果没有冲突标记的结果就是一次合格的赋值。标记中需要用到的逼迫规则有下:

那么这个算法能判断所有的公式吗?答案是否定的!对于形如¬(φ1 ∧ φ2)这样的公式无法判断(自己试一下)。

 

上述算法是一个线性时间算法。我们还有一个三次多项式时间算法。算法的主要思想:

1.任选一个未标记结点试探标记T,运行线性时间求解算法.若报告可满足,则输出可满足指派并停机;若算法报告失败或报告不可满足(矛盾),而不再有待试探的结点,算法报告”标记失败”并停机;否则转2.

2.对该结点标记F,运行线性时间求解算法.若报告可满足,则输出可满足指派并停机;若算法报告不可满足且在前面标记该结点时也报告不可满足,则报告不可满足并停机;否则将两次试探标记都相同的结点标记作为永久标记.转1.

这个算法也不是万能的,比如它对于下图语法树对应的CNF不能判定:

 SAT问题目前依然是逻辑界和计算理论界的研究热点。有兴趣的可以关注一下。

 

命题逻辑公式是否定理最起码可以通过真值表查看是否可满足,那么对于谓词逻辑公式呢?我们是不是有其他什么方法可以判断谓词逻辑公司是否有效呢?

答案是否定的:给定一个谓词逻辑公式φ,|=φ是否有效是不可判定的。这有点震惊了,到底是啥意思呢?

我们采用问题归约技术:将一个已知不可判定问题归约到所考虑的判定问题,使得要考虑的判定问题可判定必导致已知的不可判定问题成为可判定问题,这就导致了矛盾。这证明我们要考虑的判定问题是不可判定的。(如果没有学过算法的,可以先花点时间了解下什么是规约)

那么哪个判定问题是不可判定问题呢?我们选择著名的波斯特对应问题(Post Correspondence Problem, PCP,你可以先百度一下):PCP的一个问题实例由某个字母表Σ上串的两个表组成,这两个表的长度相等,一般称为A表和B表。对于某个正整数k,A=(s1,s2,...,sk),B=(t1,t2,...,tk)。(si, ti)表示一个对应对。如果存在整数序列i1,i2,...,in,当把这个序列解释成A表和B表中串的下标时,能够产生相同的串,则说这个PCP问题实例有解。i1,i2,...,in称为这个问题的一个解。PCP问题就是对于一个PCP实例,它是否有解

波斯特对应问题是不可判定的。可以参考《自动机理论、语言和计算导论》John E. Hopcroft  Rejeev Motwani Jeffrey D.Ullman著, 刘田、姜晖、王捍贫译,机械工业出版社,2004年6月第1版。

看一个波斯特对应问题实例:字母表Σ={0,1}。

例1.  A={1,10,011}, B={101,00,11},其解为:(1,3,2,3),串是1011  10  011。

例2.  A={1,10111,10},B={111,10,0},其解为(2,1,1,3)或(2,1,1,3,2,1,1,3)

例3.  A={10,011,101},B={101,11,011} 这个PCP问题实例无解

(你说什么?你感觉这个问题很简单,能够设计出算法?那你可以试试。)

 

定理 谓词逻辑公式的有效性判定问题是不可判定的:不存在判定算法,使得对于任给谓词逻辑公式Ф,判定是否|=Ф是有效的。

证明: 采用归约技术对于给定的波斯特对应问题实例C,构造一个谓词逻辑公式Ф,且构造在有限的空间和时间内完成,使得|=Ф有效当且仅当波斯特对应问题实例C有解

设波斯特对应问题实例C:

 构造公式Ф:函数符号F={e,f0 ,f1},e是常量,e,f0 ,f1是一元函数。谓词符号P。



 


 



 

 

 

  • 大小: 2.8 KB
  • 大小: 21.1 KB
  • 大小: 25.4 KB
  • 大小: 8.4 KB
  • 大小: 925 Bytes
  • 大小: 5.2 KB
  • 大小: 2.5 KB
  • 大小: 10.3 KB
  • 大小: 3.9 KB
  • 大小: 6.3 KB
  • 大小: 5.6 KB
  • 大小: 7.5 KB
  • 大小: 3.7 KB
  • 大小: 4.3 KB
  • 大小: 7.2 KB
分享到:
评论

相关推荐

    命题逻辑和谓词逻辑

    《命题逻辑和谓词逻辑》 在探讨命题逻辑与谓词逻辑之前,首先要理解逻辑的基础概念。逻辑,作为研究事物规律和思维规律的学科,是数理逻辑的主要研究对象。数理逻辑通过数学方法深入剖析逻辑的本质,它涉及到一系列...

    基于谓词逻辑的归结原理实验

    子句是一组析取项(OR连接的原子公式),通常表示为CNF(合取范式),即所有的前提都以否定形式出现,并通过AND连接。 2. 替换(Substitution):这是归结中的一个重要操作,通过将一个变量替换为一个项(可以是...

    人工智能谓词逻辑归结问题的推理系统

    人工智能中的谓词逻辑归结是一种重要的推理方法,它在理解复杂知识表示、自动推理和解决数学及逻辑问题中发挥着核心作用。谓词逻辑归结是建立在逻辑基础之上的,特别是弗雷格的算术基础和希尔伯特的形式主义之上。这...

    一阶谓词逻辑和知识绑定

    "一阶谓词逻辑和知识绑定" 一阶谓词逻辑是人工智能较早期的方法之一,基于谓词逻辑的推理是通过对函数形式的命题进行逻辑推理运算并求解。谓词逻辑中,命题是由谓词文字(函数)、逻辑运算符和量词组成的。逻辑...

    命题逻辑与谓词逻辑PPT课件.pptx

    本资源是关于命题逻辑和谓词逻辑的PPT课件,总共47页,覆盖了命题逻辑和谓词逻辑的基本概念、定义、公式和应用。 命题逻辑是研究具有真假意义的语句的逻辑系统。其中,原子命题是不能被进一步分解成更为简单的命题...

    人工智能 谓词逻辑

    - **前束范式**:谓词逻辑公式的标准形式之一,量词位于公式的最前端。 - **谓词知识表示**:利用谓词逻辑来表示知识的方法。通过将知识转换成谓词逻辑的形式,可以更方便地进行推理和计算。 #### 四、谓词逻辑实例...

    人工智能导论课件:第四章 谓词逻辑与归结原理.ppt

    "人工智能导论课件:第四章 谓词逻辑与归结原理" 在人工智能领域中,谓词逻辑和归结原理是两个非常重要的概念。...但是,谓词逻辑和归结原理也存在一定的局限性,例如无法解决某些复杂的证明问题等。

    广工人工智能谓词逻辑算法作业

    广工人工智能谓词逻辑算法作业 本资源是关于人工智能实验作业中的谓词逻辑归结原理实现,通过编写C++程序来完成。该程序实现了谓词逻辑算法,能够对子句集进行处理和分析。 首先,程序定义了一个名为guijie的类,...

    离散数学 谓词逻辑 习题课PPT课件.pptx

    本资源提供了一个系统的谓词逻辑知识点概述和习题,涵盖了谓词逻辑的基础知识点和应用,非常适合学习和研究离散数学和谓词逻辑的学生和研究人员。 在学习和研究谓词逻辑时,本资源提供了一个系统的概述和习题,帮助...

    第二章 谓词逻辑与归结原理

    人工智能课件,关于谓词逻辑与归结原理,在学习了离散数学的基础上,进一步深入的学习谓词逻辑,掌握人工智能的初步知识

    第二章_谓词逻辑1

    命题逻辑只能处理不包含变量的简单命题,而谓词逻辑则能够精确地表达和推理关于这些变量的复杂逻辑关系。 在命题逻辑中,最基本的单位是原子命题,它们被认为是不可再分解的。然而,这限制了其表达能力,比如数学中...

    详细关于谓词逻辑的介绍

    前束范式是将谓词公式转换成特定形式的过程,主要用于简化逻辑推理和消除量词的不确定性。前束范式将量词约束到最前面,便于进行逻辑推理。 4. **等价式与蕴涵式**:谓词逻辑中有许多等价式,如De Morgan定律、分配...

    人工智能-谓词逻辑 精品资料.pptx

    SKOLEM定理是指谓词逻辑的任意公式都可以化为与之等价的前束范式,但其前束范式不唯一。SKOLEM定理可以用来解决谓词逻辑中的各种问题,如推理、证明等。 人工智能-谓词逻辑精要是人工智能领域中的一种重要技术,...

    谓词逻辑离散数学

    谓词逻辑离散数学

    人工智能课件:第三章 谓词逻辑与搜索原理.pdf

    谓词逻辑是逻辑学的一部分,研究的是在命题逻辑基础上,引入谓词和量词,来描述事物之间的关系和性质的逻辑系统。搜索原理是人工智能中常用的搜索算法,用于解决复杂问题。 命题逻辑 命题逻辑是逻辑学的一部分,...

    离散数学 谓词逻辑

    ### 离散数学之谓词逻辑知识点解析 ...通过上述分析,我们可以看到谓词逻辑不仅增强了逻辑分析的能力,还为我们提供了一套系统的方法来准确地描述和分析逻辑问题。这对于进一步理解和掌握逻辑学原理至关重要。

    命题逻辑和谓词逻辑习题课的题目及参考答案.doc

    6. **主合取式**(Disjunctive Normal Form, DNF)与主析取式(Conjunctive Normal Form, CNF):这两种形式用于表示命题逻辑公式,前者是由字面量的析取组成的合取,后者是由字面量的合取组成的析取。 ### 二、...

    谓词逻辑与推理

    谓词逻辑推理,人工智能的基本理论,为人工智能系统的开发奠定了一定的理论基础

    人工智能知识表示方法谓词逻辑70 精品资料.pptx

    在谓词逻辑法中,主要研究推理的有效性,即:能否根据一些合适公式(前提)推导出新的合适公式(结论)。谓词逻辑法具有较强的表达能力,能够表达比较复杂的问题。 谓词逻辑法是人工智能知识表示方法中的一个重要...

Global site tag (gtag.js) - Google Analytics