基于动态描述逻辑DDL的动作理论

基于一阶谓词逻辑或高阶逻辑的动作理论与采用命题语言的动作理论之间存在一个关于描述和推理能力的鸿沟;作为描述逻辑的动态扩展,动态描述逻辑DDL为基于描述逻辑的动作刻画和推理提供了一种途径.系统地研究了基于DDL的动作表示和推理问题.首先,在应用描述逻辑对静态领域知识进行刻画的基础上,引入带参数的原子动作定义式和带参数的复...     

JavaLog: a framework-based integration of Java and Prolog for agent-oriented programming

Intelligent agent development has imposed new challenges on the necessary language support. Object-oriented languages have been proposed as an appropriate tool, although logic-oriented languages are more adequate for managing mental attitudes. Multi-paradigm languages supporting encapsulation of actions, hiding of private knowledge and flexible manipulation of knowledge are, certainly, a good alternative for programming agents. However, a unique language to support flexible and efficient development of multi-agent systems confronts with the tradeoffs imposed by expressive power, efficiency and support technology. An alternative to conciliate these tradeoffs is not to think about a single language but an incrementally compatible family of agent-oriented multi-paradigm languages. In this work we present an approach based on object-oriented framework technology for integrating object and logic paradigms in such a way that new language features can be incrementally added to the core language. This core language is based on logic modules integrated as object abstractions in the object paradigm. JavaLog is a materialization of this framework integrating Java and Prolog. This core was extended to provide multi-threading support, mobility and temporal-logic operators to Prolog. MoviLog, the mobile part of the family provides a novel mobility mechanism, reactive mobility by failure, which enables virtual Prolog databases distributed across Web sites.     

Multi-Agent Dynamic Logics with Informational Test

This paper investigates a family of logics for reasoning about the dynamic activities and informational attitudes of agents, namely the agents' beliefs and knowledge. The logics are based on a new formalisation and semantics of the test operator of propositional dynamic logic and a representation of actions which distinguishes abstract actions from concrete actions. The new test operator, called informational test, can be used to formalise the beliefs and knowledge of particular agents as dynamic modalities. This approach is consistent with the formalisation of the agents' beliefs and knowledge as K(D)45 and S5 modalities. Properties concerning informativeness, truthfulness and preservation of beliefs are proved for a derivative of the informational test operator. It is shown that common belief and common knowledge can be expressed in the considered logics. This means, the logics are more expressive than propositional dynamic logic with an extra modality for belief or knowledge. The logics remain decidable and belong to 2EXPTIME. Versions of the considered logics express natural additional properties of beliefs or knowledge and interaction of beliefs or knowledge with actions. It is shown that a simulation of PDL can be constructed in one of these extensions.     

Model Checking Markov Chains with Actions and State Labels

In the past, logics of several kinds have been proposed for reasoning about discrete-time or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state properties and action sequences. For this purpose, we introduce the logic as CSL which provides a powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic CSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state formulas. Thus, the truth value of path formulas depends not only on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero, we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated with an elaborate model of a scalable cellular communication system, for which several properties are formalized by means of asCSL formulas and checked using the new procedure     

A preferential semantics for causal reasoning about action

One of the principal concerns in the research area of Reasoning about Action is determining the ramifications of actions in changing environments. A particular tendency emerging in recent literature endorses the explicit incorporation of causal knowledge in logic-based action theories. It is argued that causal extensions not only enhance the expressive power of theories of action, but may also provide more concise and intuitive representations. This paper investigates semantics for causal reasoning about action and change. It does so by exploring the role of several fundamental underlying principles, such as the Principle of Minimal Change and the Principle of Causal Change. This work culminates in a general unifying semantics for a class of action theories represented by a number of recent and influential approaches – in particular, the causal relationship approach of Thielscher and the causal systems with fixed-points suggested by McCain and Turner. The unifying augmented preferential semantics, emerging as a result of this study, captures both Principles of Change and shows their clear and distinct roles.     

Answer set programming for collaborative housekeeping robotics: representation, reasoning, and execution

Answer set programming (ASP) is a knowledge representation and reasoning paradigm with high-level expressive logic-based formalism, and efficient solvers; it is applied to solve hard problems in various domains, such as systems biology, wire routing, and space shuttle control. In this paper, we present an application of ASP to housekeeping robotics. We show how the following problems are addressed using computational methods/tools of ASP: (1) embedding commonsense knowledge automatically extracted from the commonsense knowledge base ConceptNet, into high-level representation, and (2) embedding (continuous) geometric reasoning and temporal reasoning about durations of actions, into (discrete) high-level reasoning. We introduce a planning and monitoring algorithm for safe execution of plans, so that robots can recover from plan failures due to collision with movable objects whose presence and location are not known in advance or due to heavy objects that cannot be lifted alone. Some of the recoveries require collaboration of robots. We illustrate the applicability of ASP on several housekeeping robotics problems, and report on the computational efficiency in terms of CPU time and memory.     

Horn-Extended DL的Tableau算法研究

描述逻辑和逻辑程序是两种非常重要的知识表达形式,分别具有不同的表达能力。为了保证结合描述逻辑和逻辑程序的可判定性,Motik给出了一种DL-safe规则。在Motik工作的基础上,提出了对描述逻辑进行Horn子句拓展的Horn-Extended DL,并给出了Horn-Extended DL的Tableau算法,最后通过一个算例验证了算法的正确性和效率。     

Probabilistic Logic over Paths

We introduce a probabilistic modal logic PPL extending the work of [Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo. A logic for reasoning about probabilities. Information and Computation, 87(1,2):78–128, 1990; Ronald Fagin and Joseph Y. Halpern. Reasoning about knowledge and probability. Journal of the ACM, 41(2):340–367, 1994] by allowing arbitrary nesting of a path probabilistic operator and we prove its completeness. We prove that our logic is strictly more expressive than other logics such as the logics cited above. By considering a probabilistic extension of CTL we show that this additional expressive power is really needed in some applications.     

动态描述逻辑的Tableau判定算法

动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法.     

The logic of totally and partially ordered plans: a deductive database approach

The problem of finding effective logic-based formalizations for problems involving actions remains one of the main application challenges of non-monotonic knowledge representation. In this paper, we show that complex planning strategies find natural logic-based formulations and efficient implementations in the framework of deductive database languages. We begin by modeling classical STRIPS-like totally ordered plans by means of Datalog_{1 S} programs, and show that these programs have a stable model semantics that is also amenable to efficient computation. We then show that the proposed approach is quite expressive and flexible, and can also model partially ordered plans, which are abstract plans whereby each plan stands for a whole class of totally ordered plans. This results in a reduction of the search space and a subsequent improvement in efficiency.     

Using a Continuation Twice and Its Implications for the Expressive Power of call/cc

We study the implications for the expressive power of call/cc of upward continuations, specifically the idiom of using a continuation twice. Although such control effects were known to Landin and Reynolds when they invented J and escape, the forebears of call/cc, they still act as a conceptual pitfall for some attempts to reason about continuations. We use this idiom to refute some recent conjectures about equivalences in a language with continuations, but no other effects. This shows that first-class continuations as given by call/cc have greater expressive power than one would expect from goto or exits.     

INCREMENTAL LEARNING OF PROCEDURAL PLANNING KNOWLEDGE IN CHALLENGING ENVIRONMENTS

Autonomous agents that learn about their environment can be divided into two broad classes. One class of existing learners, reinforcement learners, typically employ weak learning methods to directly modify an agent's execution knowledge. These systems are robust in dynamic and complex environments but generally do not support planning or the pursuit of multiple goals. In contrast, symbolic theory revision systems learn declarative planning knowledge that allows them to pursue multiple goals in large state spaces, but these approaches are generally only applicable to fully sensed, deterministic environments with no exogenous events. This research investigates the hypothesis that by limiting an agent to procedural access to symbolic planning knowledge, the agent can combine the powerful, knowledge-intensive learning performance of the theory revision systems with the robust performance in complex environments of the reinforcement learners. The system, IMPROV, uses an expressive knowledge representation so that it can learn complex actions that produce conditional or sequential effects over time. By developing learning methods that only require limited procedural access to the agent's knowledge, IMPROV's learning remains tractable as the agent's knowledge is scaled to large problems. IMPROV learns to correct operator precondition and effect knowledge in complex environments that include such properties as noise, multiple agents and time-critical tasks, and demonstrates a general learning method that can be easily strengthened through the addition of many different kinds of knowledge.     

A semantic characterization of a useful fragment of the situation calculus with knowledge

The situation calculus, as proposed by McCarthy and Hayes, and developed over the last decade by Reiter and co-workers, is reconsidered. A new logical variant called ES is proposed that captures much of the expressive power of the original, but where certain technical results are much more easily proved. This is illustrated using two existing non-trivial results: the determinacy of knowledge theorem of Reiter and the regression theorem, which reduces reasoning about the future to reasoning about the initial situation. Furthermore, we show the correctness of our approach by embedding ES in Reiter's situation calculus.     

Hoare vs Milner: Comparing Synchronizations in a Graphical Framework With Mobility

We compare the expressive power of Hoare (i.e., CSP style) and Milner (i.e., CCS style) synchronizations for defining graph transformations in a framework where edges can perform actions on adjacent nodes to synchronize their evolutions. Furthermore, nodes can be communicated and merged. We show that the expressive powers of the two synchronization models are different, but no one is greater than the other. Finally, we show that in many interesting cases the behaviour of a synchronization model can be mimicked by the other one using suitable translations for the rewritten graphs.     

vCGG:一种基于虚结点的空间图文法形式框架

作为一种二维的形式化方法,图文法为可视化语言提供了直观而规范的描述手段.然而,大多数图文法形式框架在空间语义处理能力方面有所不足,影响了图文法的表达能力及其实际应用范围.针对现存的问题,构建了一种新型空间图文法形式框架vCGG （virtual-node based coordinate graph grammar）.区别于其他空间图文法,vCGG在产生式中通过定义虚结点的概念描述产生式与主图之间的语法结构与空间语义关系,在保留抽象能力的同时,提高了其空间语义配置性能.通过与几种典型空间图文法框架比较,vCGG形式框架在直观性、规范性、表达能力以及分析效率方面均有着较好的表现.