QQ客服 官方微博 反馈留言

题名	标记逻辑程序理论研究:说明语义与过程语义
作者	周生炳
学位类别	工学博士
答辩日期	1994-08-01
授予单位	中国科学院自动化研究所
授予地点	中国科学院自动化研究所
导师	戴汝为
关键词	非单调推理 容错推理 标记逻辑程序 支持模型 诱导序列 不循环程序 多次极限 多重极限 表达式的复盖 分解和划分 SLD-博弈树 删除策略 依赖团 nonmonotonic reasoning error-tolerated reasoning annotated logic program acyclic program supported model induced sequence coveri
学位专业	模式识别与智能系统
中文摘要	不完全性和不一致性是常识的两个主要特征，以往的工作大都独立 地研究其中的一个，分别发展为不完全信息下的非单调推理和不一致信 息下的容错推理(超协调推理)。本文提出一个基于标记逻辑的逻辑程序 理论(Annotated Logic Program，以下简称ALP)，把非单调推理和容错推 理纳入统一的框架，具有良好的说明语义和过程语义，并有简洁、方便、 灵活、便于修改、符合直觉、易于实现等特点，在新的意义上解决了非单 调推理的多扩张问题。 在说明语义方面，我们提出自由子句分析法。引入诱导序列及其极 限的概念，给出极限存在的一个等价条件。然后，我们提出一系列新的概 念和工具，对自由子句进行细致的分析。针对自由子句的不同情况，本文 证明不循环程序存在唯一的支持模型： 1． 对复盖程序G，它的支持模型是任意Herbrand解释的诱导序列 的极限。 2． 如果G中含k个自由子句，并且这k个子句头中出现的文字不 含自反依赖关系，则它的k次极限就是其支持模型。 3． 对一般的不循环程序，它的支持模型是其k次多重极限，其中k 是程序中自由子句的个数。 作为ALP过程语义的理论基础，本文建立了Herbrand域上的表达 式理论。我们提出表达式复盖、分解和划分的概念，建立分解和划分表达 式的算法，以及若干表达式复盖的判别准则。 在过程语义方面，我们把传统逻辑程序的SLD-归结改造为SLD- 博弈树。对有限树，在它上面施行一种特殊的删除策略，可确定复盖程序 的支持模型。我们提出SLD-博弈树的成功集的概念，利用该概念证明 了计算规则的独立性。对无穷树，本文提出依赖团及其伴随集的概念，证 明依赖团中元素的值由其伴随集中元素的值决定，并据此提出几种常见 情形的无穷树的有限化方法。对一般的无穷树，能否化简以及如何化简 的问题尚待解决。
英文摘要	Incompleteness and inconsistency are the twe main features of common- sense. Nonmonotonic reasoning under incomplete information and error--toler- ated reasoning (paraconsistent logics) with inconsistent information have been independently developed to formalize: one of them respectively. In this paper, we propose a logic program based on annotated logic Annotated Logic Pro> gram, henceforth ALP which provides a unified formalism for the two kinds of reasoning mentioned above. Our ALP possesses a well--founded declar- ative semantics and procedural semantics. It is flexible, convenient,and succinct for commonsense representation, and, is not puzzled by the notorious multiple ex- tensions problem of nonmonotonie reasoning. The declarative semantics of ALP is given with free clauses analysis method presented in this paper. We define the induced sequence and its limit, establish a sufficient and necessary condition for the existence of latter. Having carefully analysed the free clauses, we show that every aeyclie program has one and only one Herbrand supported model according to different cases of the free clauses: 1. For covered program,its supported model is the limit of an interpretation sequence induced by any Herbrand :interpretation. 2. If there is not reflexive dependent relation among the head literais of the all k free clauses occurred in the program,then the k--th limit is its supported model. 3. For the general acyclic program G, the supported model of it is turned out to be its k-th multi/irnit,where k is just the number of the free clauses of G. To lay a foundation of procedural semantics of ALP, we establish an expres- sion theory based on the Herbrand field. The concepts of covering, decomposi- tion, and partition of expressions is lpresented. Correspondingly, algorithms of de~ composing or partioning expressions is described, and sereval criteria to judge whether one or more than one expressions cover another one are provided. About the procedural semantics of ALP,we propose the concept of the SLD --game tree of a query. A deletion strategy for the finite SLD--game tree which can determine the supported model of the covered acyclic ALP is first giv- en, then independence of the computation rule is proved. Finally, we define the dependent cluster of a literal and its accompanied set,and show that the value of the elements of the dependent cluster in the supported model is decided by that of the elements of its accompanied set. As a result,simplification of several common cases of infinite SLD--garne trees is performed. However ,how to sim- plify the general infinite SLD--garne tree is an open problem.
语种	中文
其他标识符	300
内容类型	学位论文
源URL	[http://ir.ia.ac.cn/handle/173211/5645]
专题	毕业生_博士学位论文
推荐引用方式 GB/T 7714	周生炳. 标记逻辑程序理论研究:说明语义与过程语义[D]. 中国科学院自动化研究所. 中国科学院自动化研究所. 1994.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。