Reasoning about Minimal Knowledge in Nonmonotonic Modal Logics

We study the problem of embedding Halpern and Moses's modal logic of minimal knowledge states into two families of modal formalism for nonmonotonic reasoning, McDermott and Doyle's nonmonotonic modal logics and ground nonmonotonic modal logics. First, we prove that Halpern and Moses's logic can be embedded into all ground logics; moreover, the translation employed allows for establishing a lower bound (3p) for the problem of skeptical reasoning in all ground logics. Then, we show a translation of Halpern and Moses's logic into a significant subset of McDermott and Doyle's formalisms. Such a translation both indicates the ability of Halpern and Moses's logic of expressing minimal knowledge states in a more compact way than McDermott and Doyle's logics, and allows for a comparison of the epistemological properties of such nonmonotonic modal formalisms.     

Negation as Failure as Resolution

Providing a clean procedural semantics of the Negation As Failure rule in Logic Programming has been an open problem for some time now. This rule has been treated as a technique in nonmonotonic reasoning, not as a rule in classical logic. This paper contains a demonstration of the negation as failure rule as a resolution procedure in first-order logic. We present a sound and complete resolution scheme for negation as failure rule for the larger class of constraint logic programs. The approach is to consider a canonical partition of the completion of a definite (constraint) program into the IF and the FI programs. We show that a negated goal, provable from the completed definite program is provable from just the FI part. The clauses in this program have a structure dual to that of definite Horn clauses. We describe a sound and complete linear resolution rule for this fragment, and show that a resolution proof of the negated goal from the FI part corresponds to a finite failure tree resulting from classical linear resolution applied to the goal on the If part of the original definite program. Our work shows that negation as failure rule can be computationally efficient in the sense that the SLD-resolution on the If part of a definite program along with the negation as failure rule is more efficient than a direct resolution procedure on the completion of that program.     

'Classical' Negation in Nonmonotonic Reasoning and Logic Programming

Gelfond and Lifschitz were the first to point out the need for a symmetric negation in logic programming and they also proposed a specific semantics for such negation for logic programs with the stable semantics, which they called 'classical'. Subsequently, several researchers proposed different, often incompatible, forms of symmetric negation for various semantics of logic programs and deductive databases. To the best of our knowledge, however, no systematic study of symmetric negation in non-monotonic reasoning was ever attempted in the past. In this paper we conduct such a systematic study of symmetric negation. We introduce and discuss two natural, yet different, definitions of symmetric negation: one is called strong negation and the other is called explicit negation. For logic programs with the stable semantics, both symmetric negations coincide with Gelfond–Lifschitz' 'classical negation'. We study properties of strong and explicit negation and their mutual relationship as well as their relationship to default negation 'not', and classical negation '¬'. We show how one can use symmetric negation to provide natural solutions to various knowledge representation problems, such as theory and interpretation update, and belief revision. Rather than to limit our discussion to some narrow class of nonmonotonic theories, such as the class of logic programs with some specific semantics, we conduct our study so that it is applicable to a broad class of non-monotonic formalisms. In order to achieve the desired level of generality, we define the notion of symmetric negation in the knowledge representation framework of AutoEpistemic logic of Beliefs, introduced by Przymusinski.     

多智能体系统中并发动态知识、信念和肯定性逻辑的研究

将知识、信念和肯定性逻辑从单个智能体扩展到多智能体系统,并且实现了多智能体系统中知识、信念和肯定性逻辑与具有并发动态属性的行为之间的很好结合.以此为基础,提出了多智能体系统中并发动态知识、信念和肯定性逻辑,简称CDKBC逻辑.为了对CDKBC逻辑进行解释,也给出了CDKBC模型,并且讨论了知识、信念和肯定性之间的关系,即知识蕴涵着肯定性,肯定性蕴涵着信念.文中也给出了一个相应的证明系统(即公理系统),证明了该系统是可靠的和完备的,并且证明了系统的有效性问题是EXPTIME完全的.最后论文给出了CDKBC逻辑的实例.     

A LOGIC OF ARGUMENTATION FOR REASONING UNDER UNCERTAINTY

We present the syntax and proof theory of a logic of argumentation, LA. We also outline the development of a category theoretic semantics for LA. LA is the core of a proof theoretic model for reasoning under uncertainty. In this logic, propositions are labeled with a representation of the arguments which support their validity. Arguments may then be aggregated to collect more information about the potential validity of the propositions of interest. We make the notion of aggregation primitive to the logic, and then define strength mappings from sets of arguments to one of a number of possible dictionaries. This provides a uniform framework which incorporates a number of numerical and symbolic techniques for assigning subjective confidences to propositions on the basis of their supporting arguments. These aggregation techniques are also described with examples.     

Cooperation Protocols in Multi-Agent Robotic Systems

Multi-agent robotic systems are useful in many practical applications. For some tasks, such as holding a conference, cooperation among agents are necessary. For other tasks, such as cleaning a room, multiple agents can work in parallel for better performance. This paper provides help-based (HCP) and coordination-based (CCP) protocols for controlling agents to accomplish multi-agent tasks. The HCP utilizes efficient negotiation to coordinate agents into groups. The CCP improves overall performance by exchanging local knowledge among agents and making decisions in parallel. A reactive and modularized agent architecture was employed to implement the protocols. Since each protocol is embedded into the architecture, it is efficient and effective. In addition, the protocols are deadlock-free. The protocols were utilized to solve the Object-Sorting Task, which abstracts two characteristics of tasks: parallelism and cooperation. The experimental results showed that 1) both HCP and CCP are stable under different workload; 2) the protocols can effectively utilize the agent-power to achieve super-linear improvement; 3) The CCP is better than the HCP in both performance and speedup.     

多Agent系统中的常识和分布式知识

Agent的形式化研究已成为人工智能、哲学逻辑和计算语言学共同关心的重要课题,有着广泛的应用。逻辑学的理论为人工智能的发展提供了有力的工具。介绍了Agent系统设计的逻辑学基础,以及模态逻辑和认知逻辑,在此基础之上重点介绍了多Agent系统中的常识和分布式知识。     

Strong Negation and Equivalence in the Safe Belief Semantics

The safe belief semantics uses intermediate logics to definean extension of answer sets to all propositional formulas, butonly considering one kind of negation. In this work we extendsafe beliefs adding the strong negation connective. The mainfeature of our extension is that strong negation can occur beforeany formula, and not only at the atomic level. We give resultsconcerning the relation between strong negation extensions ofintermediate logics and safe beliefs and consider the way inwhich strong negation can be eliminated from any formula whilepreserving its semantics. We also propose two new notions ofequivalence: substitution equivalence and contextualized equivalence.We prove that they are both more general than strong equivalenceand, for propositional formulas where strong negation may occurat the non-atomic level, substitution equivalence captures anotion of equivalence that cannot be captured by strong equivalencealone.     

An Interpretation of Default Logic in Minimal Temporal Epistemic Logic

When reasoning about complex domains, where information available is usually only partial, nonmonotonic reasoning can be an important tool. One of the formalisms introduced in this area is Reiter's Default Logic (1980). A characteristic of this formalism is that the applicability of default (inference) rules can only be verified in the future of the reasoning process. We describe an interpretation of default logic in temporal epistemic logic which makes this characteristic explicit. It is shown that this interpretation yields a semantics for default logic based on temporal epistemic models. A comparison between the various semantics for default logic will show the differences and similarities of these approaches and ours.     

Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic

Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a system, is explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence.     

异构多智能体系统模型检查

近几年,模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑（ATL）,也被给予了高度关注.根据智能体是否可以看到全局信息分为不完全信息和完全信息;根据智能体是否可以记录历史信息分为无记忆能力和无限记忆能力,提出了四种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而,在一个多智能体系统中,考虑完全信息和无限记忆能力时,所有智能体都只能选择这一种策略类型;在考虑不完全信息或无记忆能力时,仅在联合模态操作<>φ和的[[A]]φ里出现的智能体具备这种策略类型,而其他智能体还是完全信息和无限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致,且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中,智能体的策略类型往往取决于系统本身,且不同智能体具有不同的策略类型,即智能体策略类型是异构的,这种多智能体系统被称为异构多智能体系统.针对这些问题,本文提出了一种在语法层对智能体策略类型进行刻画的系统模型,即带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入"策略类型"这一属性,允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对新提出的系统模型,对ATL语义进行了研究,设计了ATL模型检查算法,实现了相应的模型检查工具ShTMC.     

Rights and Argumentation in Open Multi-Agent Systems

As utility calculus cannot account for an important part of agents' behaviour in Multi-Agent Systems, researchers have progressively adopted a more normative approach. Unfortunately, social laws have turned out to be too restrictive in real-life domains where autonomous agents' activity cannot be completely specified in advance. It seems that a halfway concept between anarchic and off-line constrained interaction is needed. We think that the concept of right suits this idea. Rights improve coordination and facilitate social action in Multi-Agent domains.Rights allow the agents enough freedom, and at the same time constrain them (prohibiting specific actions). Besides, rights can be understood as the basic concept underneath open normativesystems where the agents reason about the code they must abide by. Typically, in such systems this code is underspecified. On the other hand, the agents might not have complete knowledge about the rules governing their interaction. Conflict situations arise, thus, when the agents have different points of view as to how to apply the code. We have extended Parsons's et al. argumentation protocol (Parsons et al. 1998a, b) to normative systems to deal with this problem.     

有界模型检测同步多智体系统的时态认知逻辑

提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(bounded model checking,简称BMC)算法.基于同步解释系统语义,在时态逻辑CTL*的语言中引入认知模态词,从而得到一个新的时态认知逻辑ECKL_n.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.ECKL_n的时态认知表达能力强于另一个逻辑CTLK.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.     

Possible events, actual events, and robots

To plan means reasoning about possible actions, but a robot must also reason about actual events. This paper proposes a formal theory about actual and possible events. It presents a new modal logic as a notation for this theory and a technique for planning in the modal logic using a first-order theorem prover augmented with simple modal reasoning. This avoids the need for a general modal-logic theorem prover. Adding beliefs to this theory raises an interesting problem for which the paper offers a tentative solution.