【作者】 周勇；

【导师】 朱梧槚；

【作者基本信息】 南京航空航天大学 ， 计算机应用技术， 2006， 博士

【摘要】 非单调推理是人工智能领域中一类重要的常识推理,其中包含缺省逻辑、自认知逻辑等内容。自认知逻辑的稳定集和扩充可用于刻划主体(agent)的推理能力以及认知状态,是自认知逻辑重要的研究内容。本文给出了稳定集的一种等价表示方法,该方法可以比较简洁、统一地描述多自认知逻辑中的相关概念。在多自认知逻辑中,本文基于对主体之间认知能力的不同假设,提出了四种稳定集,讨论了它们之间的关系,并以一种稳定集为例,给出了其语义表示,并引入了相应的扩充概念。另外,文中也讨论了一种可以描述环境的扩充。自认知逻辑程序可以看成是自认知逻辑的一种简化,可以比较方便地用于推理。本文分别讨论了单主体和多主体的自认知逻辑程序。对于单主体的情形,给出了一种不动点语义,证明了它和完全Bonatti稳定集等价,并可以转化为扩展逻辑程序的回答集语义。对于多主体的情形,根据对主体认知情况的不同处理,提出了两类稳定集:P稳定集和广义稳定集。在给出了多自认知逻辑程序的三值语义模型后,证明了该语义是和广义稳定集相互对应的。而当三值语义简化为二值时,对应的是P稳定集。P稳定集可看成是自认知逻辑程序中稳定集的自然推广,而广义稳定集可看成是Bonatti稳定集的推广。对于有序逻辑程序,本文基于不动点原理,提出了处理优先序的新方法,统一了多种已有的回答集语义,得到了一类新的回答集语义。通过证明和举例详细比较了各种回答集语义之间的强弱关系,给出了它们在集合包含关系意义下的哈斯图,证明了各种回答集语义在包含关系下形成格的结构。安全协议是保证网络通信安全的重要内容。形式化方法是验证安全协议的一种重要方法。本文提出了一种复合型安全协议,在同一协议中结合了在线可信第三方和离线可信第三方两种通信方式。对SVO逻辑和Kailar逻辑进行扩充,增强其表达能力,特别是非单调推理能力,给出了协议验证的新方法。另外,作为逻辑程序的一种应用,本文也提出了基于多自认知逻辑程序的验证方法,并以KM等协议为例,验证了协议的非否认性和公平性等性质。更多还原

【Abstract】 Nonmonotonic reasoning systems including default logic and autoepistemic logic are important in the commonsense reasoning of artificial intelligence.The stable sets and expansions of autoepistemic logic are important to denote the reasoning ability and the epistemic status of the agent. A new characterization of the stable sets of the autoepistemic logic is given and it can be extended to multi-autoepistemic logic easily.There are different cases of the epistemic ability between the agents in the multi-autoepistemic logic. Based on the different assumptions of the epistemic ability four kinds of the stable sets are introduced and their relationship are discussed. The corresponding expansions and semantics of multi-autoepistemic logic are also given. Moreover, a kind of expansion in which the environment can be described is presented too.Autoepistemic logic program is a simplification of the autoepistemic logic. The single agent and multi-agent autoepistemic logic program are introduced. For the single agent case, a fixed-point semantics which can be translated to the answer set semantics of the general logic program is given and is proved equivalent to the complete Bonatti stable set. For the multi-agent case, two kinds of stable sets are discussed, that is the P stable set and the general stable set. The three-value semantics for the multi-agent autoepistemic logic program corresponds to general stable semantics and the simplified two-value semantics corresponds to the P stable set. P stable set can be viewed as the generalization of the stable set in autoepistemic logic and general stable set can be viewed as the generalization of the Bonatti stable set in autoepistemic logic.Based on the fixpoint principle, some new methods are introduced to treat the prior orders among the rules in ordered logic program. That results in a new class of answer set semantics for ordered logic program including several kinds of already existed semantics. The diverse answer set semantics are compared in detail and a Hasse diagram with respect to set inclusive relations for the semantics is given. It is proved that the answer set semantics form a lattice structure.Security protocols are important for the security of the network communications and formal methods are important for verifying the security protocols. Combined with the online trusted third part(TTP) protocol and the off-line TTP protocol, a new compound security protocol is introduced. Based on the extended systems of SVO logic and Kailar logic which can process nonmonotonic reasoning, the new methods for the security protocol verification are given. Moreover, the verification methods using general logic program and multi-agent autoepistemic logic program are also discussed. With these new methods, some non-repudiation protocols are proved to have the property of non-repudiation and fairness.更多还原