关于三值逻辑程序中否定和蕴涵完备化程序的不动点语义

来源 :计算机科学 | 被引量 : 0次 | 上传用户：zjwx2008

【摘要】

：

逻辑程序具有丰富的表达能力和非确定性等特点，在定理机器证明、关系数据库系统、程序验证、模块化程序设计和非单调推理等方面都有了广泛的应用。本文是继续文[8]的工作。首

【作者】

：

刘富春

【机构】

：

广东工业大学应用数学学院,中山大学计算机系

【出处】

：

计算机科学

【发表日期】

：

2006年4期

【关键词】

：

逻辑程序否定和蕴涵完备化程序 Herbrand模型后继算子 Fitting算子 Logic programming →-completion and →-

【基金项目】

：

广东省自然科学基金项目（020146,031541和广东工业大学青年基金项目（042027）.

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

逻辑程序具有丰富的表达能力和非确定性等特点，在定理机器证明、关系数据库系统、程序验证、模块化程序设计和非单调推理等方面都有了广泛的应用。本文是继续文[8]的工作。首先通过两个反例，指出了文[7]中关于否定完备化程序Comp（→，Pr）和蕴涵完备化程序Comp（→，Pr）的两个重要定理都存在一定程度的错误。然后对这两个定理进行了修改，用后继算予Tpt和Fitting算予FPr的不动点语义，分别给出了否定完备化程序（Somp（→，Pr）和蕴涵完备化程序Comp（→，Pr）的Herbrand模型的充分条件和必要

其他文献

基于网格的流媒体服务QoS管理框架及实现

流媒体服务是Internet上一类高带宽需求和高实时性约束的应用，对服务质量（Quality of Service，QoS）有较高的要求。流媒体服务的发展导致传统的QoS管理框架难以适应平台的异构性和

期刊

流媒体服务服务质量网格Stream media service Quality of Service（QoS） Grid

基于Multi—Agent的个性化远程教育系统研究

以学生为中心的个性化、交互协作式教学是远程教学的本质特征。在分析远程教育的现状基础上，论文提出了基于多代理技术的个性化远程教育系统。该系统集www技术和Agent技术与一

期刊

远程教育智能代理多代理技术Distance education Intelligent agent Multi-agent technique

一种基于关联聚类的汉语共指消解方法

指代消解是自然语言处理领域中的一个重要问题。本文引入图对汉语名词短语的指代消解问题进行建模,将指代消解问题转化为图划分问题,并应用关联聚类算法来实现对图的自动划分

期刊

指代消解共指关联聚类线性规划

计算科学的新领域：DNA计算（Ⅱ）

DNA计算是应用分子生物技术进行计算的新方法.从理论上研究DNA计算方法，有利于推动理论计算科学的发展.本系列文章应用形式语言及自动机理论技术，系统地探讨了DNA分子的可计算

期刊

DNA粘接计算模型计算能力DNA有穷自动机DNA sticker model Computational capacity DNA finite au

一种基于共轭混沌映射的数字水印算法研究

数字水印技术在多媒体方面有着广泛的应用，其中最受关注，同时也是要求最高的应用是用于版权保护的数字水印技术。本文提出了一种基于共轭的抗剪切鲁棒水印算法，运用一类标准混沌

期刊

混沌共轭映射数字水印Chaos Coupled map Digital watermarking

基于QoWS的Web服务评估算法

本文提出了一个完整的Web服务质量的评估算法。此算法在分析了Web服务评量和相对服务质量的基础之上，计算Web服务质量的综合评估值，并且建立一个Web服务质量评估模型，将此算法应

期刊

WEB服务质量Web服务评量质量评估QoWS Web service rating Quality evaluation

一种新的类BAN逻辑模态语义模型——兼论类BAN逻辑的语法缺陷

由于类BAN逻辑缺乏明确而清晰的语义，其语法规则和推理的正确性就受到了质疑。本文定义了安全协议的计算模型，在此基础上定义了符合模态逻辑的类BAN逻辑“可能世界”语义模型，并

期刊

类BAN逻辑模态逻辑形式语义BAN逻辑语义模型语法规则缺陷计算模型安全协议定义BAN-like logic Modal logic Fo

分块PCA鉴别特征抽取能力的分析研究

基于主成分分析(Principal Component Analysis,PCA),本文提出了分块 PCA 人脸识别方法。分块 PCA 从模式的原始数字图像出发,先对图像进行分块,对分块得到的子图像矩阵采用 PCA 方法进行特征抽取,从而实现模式的分类。新方法的特点是能有效地抽取图像的局部特征,正是这些特征使此类模式区别于彼类。在 Yale 人脸数据库上测试了该方法的鉴别能力。实验的结果表明,分块

期刊

线性鉴别分析主成分分析特征抽取分块主成分分析人脸识别Linear discriminant analysis （LDA） Principal com

多核、多线程处理器的低功耗设计技术研究

随着微处理器设计技术和半导体制造工艺的进步，芯片的规模和复杂度急剧增大，超高的功耗密度对系统稳定性造成很大影响，功耗壁垒已经成为提升微处理器性能的最大障碍。本文介绍了

期刊

多核多线程微处理器低功耗Multi-core Multithreading Microprocessor Low power

一种单速率组播速率控制与修剪算法

组播网络的异构性问题导致了组播内部公平性问题。本文在分析了相关工作的局限性之后，提出了一种基于效用的单速率组播内部公平性标准，其优化目标是最大化组播会话的净收益。相

期刊

单速率组播速率控制修剪Single-rate multicast Rate control Pruning

关于三值逻辑程序中否定和蕴涵完备化程序的不动点语义

与本文相关的学术论文