Search

By their very design, many robot control programs are non-terminating. This paper describes a situation calculus approach to expressing and proving properties of non-terminating programs expressed in Golog, a high level logic programming language for modeling and implementing dynamical systems. Because in this approach actions and programs are represented in classical (second-order) logic, it is natural to express and prove properties of Golog programs, including non-terminating ones, in the very same logic. This approach to program proofs has the advantage of logical uniformity and the availability of classical proof theory. [ABSTRACT FROM AUTHOR]

This article considers defeasible beliefs in dynamic settings. In particular, we examine the belief projection problem: what is believed after performing an action and/or receiving new information? The approach is based on an epistemic variant of Reiter's situation calculus, where actions not only have physical effects but may also provide new information to the agent. The preferential belief structure is initially determined using conditional statements. New information is then incorporated using two popular belief revision schemes, namely natural and lexicographic revision. The projection problem is solved twofold in this formalism: by goal regression and by knowledge base progression. [ABSTRACT FROM AUTHOR]

This research note contains an extension of a previous work by Cabalar and Santos (2011) that formalised several spatial puzzles formed by strings and holes. That approach explicitly ignored some configurations and actions that were irrelevant for the studied puzzles but are physically possible and may become crucial for other spatial reasoning problems. In particular, the previous work did not consider the formation of string loops or the situations where a holed object is partially crossed by another holed object. In this paper, we remove these limitations by treating string loops as dynamic holes that can be created or destroyed by a pair of elementary actions, respectively picking or pulling from strings. We explain how string loops can be recognised in a data structure representing the domain states and define a notation to represent crossings through string loops . The resulting formalism is dual in the sense that it also allows understanding any hole as a kind of (sometimes rigid) closed string loop. [ABSTRACT FROM AUTHOR]

We investigate agents that have incomplete information and make decisions based on their beliefs expressed as situation calculus bounded action theories. Such theories have an infinite object domain, but the number of objects that belong to fluents at each time point is bounded by a given constant. Recently, it has been shown that verifying temporal properties over such theories is decidable. We take a first-person view and use the theory to capture what the agent believes about the domain of interest and the actions affecting it. In this paper, we study verification of temporal properties over online executions. These are executions resulting from agents performing only actions that are feasible according to their beliefs. To do so, we first examine progression, which captures belief state update resulting from actions in the situation calculus. We show that, for bounded action theories, progression, and hence belief states, can always be represented as a bounded first-order logic theory. Then, based on this result, we prove decidability of temporal verification over online executions for bounded action theories. [ABSTRACT FROM AUTHOR]

This paper studies how logic-based reasoning about actions and change (RAC) with its problems of temporal projection and qualification can be formalised in terms of argumentation. In particular, we extend earlier work of translating the languagefor RAC into a logic-based argumentation framework, by introducing new types of arguments for (i) backward persistence and (ii) persistence from observations. This forms a conservative extension of the languagethat gives a semantic meaning to domains that cannot be interpreted underthus addressing further the frame and (exogenous) qualification problems. As such the paper strengthens the link between argumentation theory and RAC in artificial intelligence. [ABSTRACT FROM AUTHOR]

As a contribution to the challenge of building game-playing AI systems, we develop and analyse a formal language for representing and reasoning about strategies. Our logical language builds on the existing general Game Description Language (GDL) and extends it by a standard modality for linear time along with two dual connectives to express preferences when combining strategies. The semantics of the language is provided by a standard state-transition model. As such, problems that require reasoning about games can be solved by the standard methods for reasoning about actions and change. We also endow the language with a specific semantics by which strategy formulas are understood as move recommendations for a player. To illustrate how our formalism supports automated reasoning about strategies, we demonstrate two example methods of implementation: first, we formalise the semantic interpretation of our language in conjunction with game rules and strategy rules in the Situation Calculus; second, we show how the reasoning problem can be solved with Answer Set Programming. [ABSTRACT FROM AUTHOR]

Abstract: We provide a solution to the ramification problem that integrates findings of different axiomatic approaches to ramification from the last ten to fifteen years. For the first time, we present a solution that: (1) is independent of a particular time structure, (2) is formulated in classical first-order logic, (3) treats cycles – a notoriously difficult aspect – properly, and (4) is assessed against a state-transition semantics via a formal correctness proof. This is achieved as follows: We introduce indirect effect laws that enable us to specify ramifications that are triggered by activation of a formula rather than just an atomic effect. We characterise the intended models of these indirect effect laws by a state-transition semantics. Afterwards, we show how to compile a class of indirect effect laws into first-order effect axioms that then solve the ramification and frame problems. We finally prove the resulting effect axioms sound and complete with respect to the semantics defined earlier. [Copyright &y& Elsevier]

Nonmonotonic causal logic is a knowledge representation language designed for describing domains that involve actions and change. The process of literal completion, similar to program completion familiar from the theory of logic programming, can be used to translate some nonmonotonic causal theories into classical logic. Its applicability is restricted, however, to theories that deal with truth-valued fluents, represented by predicate symbols. In this note we introduce functional completion—a more general process that can be applied to causal theories in which fluents are treated as functions. [ABSTRACT FROM AUTHOR]

Nonmonotonic causal logic, introduced by McCain and Turner (McCain, N. and Turner, H. 1997. Causal theories of action and change. In Proceedings of National Conference on Artificial Intelligence (AAAI), Stanford, CA, 460–465) became the basis for the semantics of several expressive action languages. McCain's embedding of definite propositional causal theories into logic programming paved the way to the use of answer set solvers for answering queries about actions described in such languages. In this paper we extend this embedding to nondefinite theories and to the first-order causal logic. [ABSTRACT FROM AUTHOR]

Logic programming is a powerful paradigm for programming autonomous agents in dynamic domains as witnessed by languages such as Golog and Flux. In this work we present ALPprolog, an expressive, yet efficient, logic programming language for the online control of agents that have to reason about incomplete information and sensing actions. [ABSTRACT FROM AUTHOR]

We start from Reiter’s solution to the frame problem in terms of successor state axioms and Scherl and Levesque’s extension to knowledge, as formulated by Lakemeyer and Levesque in their logic ES.While it was believed up to now that quantification over actions is a characteristic feature of Reiter’s solution, we here show that for a reasonably large subset of Reiter’s basic action theories one can do without.We do so by recasting restricted basic action theories in a propositional modal logic, viz. dynamic epistemic logic with public announcements and public assignments. [ABSTRACT FROM PUBLISHER]

Abstract: McCarthy''s Situation Calculus is arguably the oldest special-purpose knowledge representation formalism, designed to axiomatize knowledge of actions and their effects. Four decades of research in this area have led to a variety of alternative formalisms: While some approaches can be considered instances or extensions of the classical Situation Calculus, like Reiter''s successor state axioms or the Fluent Calculus, there are also special planning languages like ADL and approaches based on a linear (rather than branching) time structure like the Event Calculus. The co-existence of many different calculi has two main disadvantages: The formal relations among them is a largely open issue, and a lot of today''s research concerns the transfer of specific results from one approach to another. In this paper, we present a unifying action calculus, which encompasses (well-defined classes of) all of the aforementioned formalisms. Our calculus not only facilitates comparisons and translations between specific approaches, it also allows to solve interesting problems for various calculi at once. We exemplify this by providing a general, calculus-independent solution to a problem of practical relevance, which is intimately related to McCarthy''s quest for elaboration tolerant formalisms: the modularity of domain axiomatizations. [Copyright &y& Elsevier]

Abstract: We describe (), a specialized, model-theoretic logic for reasoning about actions. is able to represent non-deterministic domains involving concurrency, static laws (constraints), indirect effects (ramifications), and narrative information in the form of action occurrences and observations along a time line. We give formal results which characterize ''s high degree of modularity and elaboration tolerance, and show how these properties help to separate out, and provide principled solutions to, different aspects of the qualification problem. In particular, we identify the endogenous qualification problem as the problem of properly accounting for highly distributed, and potentially conflicting, causal knowledge when reasoning about the effects of actions. We show how a comprehensive solution to the endogenous qualification problem helps simplify the exogenous qualification problem — the problem of reconciling conflicts between predictions about what should be true at particular times and actual observations. More precisely, we describe how is able to use straightforward default reasoning techniques to solve the exogenous qualification problem largely because its robust treatments of the frame, ramification and endogenous qualification problems combine into a particular characteristic of elaboration tolerance that we formally encapsulate as a notion of “free will”. [Copyright &y& Elsevier]

Abstract: In reasoning about actions, it is commonly assumed that the dynamics of domains satisfies the Markov Property: the executability conditions and the effects of all actions are fully determined by the present state of the system. This is true in particular in Reiter''s Basic Action Theories in the Situation Calculus. In this paper, we generalize Basic Action Theories by removing the Markov property restriction, making it possible to directly axiomatize actions whose effects and executability conditions may depend on past and even alternative, hypothetical situations. We then generalize Reiter''s regression operator, which is the main computational mechanism used for reasoning with Basic Action Theories, so that it can be used with non-Markovian theories. [Copyright &y& Elsevier]

Abstract: This special issue is dedicated to John McCarthy, founding father of Artificial Intelligence. It contains a collection of recent contributions to the field of knowledge representation and reasoning, a field that McCarthy founded and that has been a main focus of his research during the last half century. In this introductory article, we survey some of McCarthy''s major contributions to the field of knowledge representation and reasoning, and situate the papers in this special issue in the context of McCarthy''s previous work. [Copyright &y& Elsevier]

The situation calculus is a versatile logic for reasoning about actions and formalizing dynamic domains. Using the non-Markovian action theories formulated in the situation calculus, one can specify and reason about the effects of database actions under the constraints of the classical, flat database transactions, which constitute the state of the art in database systems. Classical transactions are characterized by the so-called ACID properties. With non-Markovian action theories, one can also specify, reason about, and even synthesize various extensions of the flat transaction model, generally called advanced transaction models (ATMs). In this paper, we show how to use non-Markovian theories of the situation calculus to specify and reason about the properties of ATMs. In these theories, one may refer to past states other than the previous one. ATMs are expressed as such non-Markovian theories using the situation calculus. We illustrate our method by specifying (and sometimes reasoning about the properties of) several classical models and known ATMs. [ABSTRACT FROM AUTHOR]

In this extended abstract we describe the robot programming and planning language Readylog, a Golog dialect which was developed to support the decision making of robots acting in dynamic real-time domains like robotic soccer. The formal framework of Readylog, which is based on the situation calculus, features imperative control structures like loops and procedures, allows for decision-theoretic planning, and accounts for a continuously changing world. We developed high-level controllers in Readylog for our soccer robots in RoboCup’s Middle-size league, but also for service robots and for autonomous agents in interactive computer games. [ABSTRACT FROM AUTHOR]

We present the class FDNC of logic programs that allows for function symbols (F), disjunction (D), nonmonotonic negation under the answer set semantics (N), and constraints (C), while still retaining the decidability of the standard reasoning tasks. Thanks to these features, FDNC programs are a powerful formalism for rule-based modeling of applications with potentially infinite processes and objects, and which allows also for common-sense reasoning in this context. This is evidenced, for instance, by tasks in reasoning about actions and planning: brave and open queries over FDNC programs capture the well-known problems of plan existence and secure (conformant) plan existence, respectively, in transition-based actions domains. As for reasoning from FDNC programs, we show that consistency checking and brave/cautious reasoning tasks are EXPTIME-complete in general, but have lower complexity under syntactic restrictions that give rise to a family of program classes. Furthermore, we also determine the complexity of open queries (i.e., with answer variables), for which deciding non-empty answers is shown to be EXPSPACE-complete under cautious entailment. Furthermore, we present algorithms for all reasoning tasks that are worst-case optimal. The majority of them resorts to a finite representation of the stable models of an FDNC program that employs maximal founded sets of knots, which are labeled trees of depth at most 1 from which each stable model can be reconstructed. Due to this property, reasoning over FDNC programs can in many cases be reduced to reasoning from knots. Once the knot-representation for a program is derived (which can be done off-line), several reasoning tasks are not more expensive than in the function-free case, and some are even feasible in polynomial time. This knowledge compilation technique paves the way to potentially more efficient online reasoning methods not only for FDNC, but also for other formalisms. [ABSTRACT FROM AUTHOR]

Abstract: In this paper, we present the robot programming and planning language Readylog, a Golog dialect, which was developed to support the decision making of robots acting in dynamic real-time domains, such as robotic soccer. The formal framework of Readylog, which is based on the situation calculus, features imperative control structures such as loops and procedures, allows for decision-theoretic planning, and accounts for a continuously changing world. We developed high-level controllers in Readylog for our soccer robots in RoboCup’s Middle-size league, but also for service robots and for autonomous agents in interactive computer games. For a successful deployment of Readylog on a real robot it is also important to account for the control problem as a whole, integrating the low-level control of the robot (such as localization, navigation, and object recognition) with the logic-based high-level control. In doing so, our approach can be seen as a step towards bridging the gap between the fields of robotics and knowledge representation. [Copyright &y& Elsevier]

Abstract: One of the main challenges in motor control is expressing high-level goals in terms of low-level actions. To do so effectively, motor control systems must reason about actions at different levels of abstraction. Grounding high-level plans in low-level actions is essential semantic knowledge for plan-based control of real robots. We present a robot control system that uses declarative, procedural and predictive knowledge to generate, execute and optimize plans. Declarative knowledge is represented in PDDL, durative actions constitute procedural knowledge, and predictive knowledge is learned by observing action executions. We demonstrate how learned predictive knowledge enables robots to autonomously optimize plan execution with respect to execution duration and robustness in real-time. The approach is evaluated in two different robotic domains. [Copyright &y& Elsevier]

Abstract: In this paper, we study the following basic problem: After having executed a sequence of actions, find a sequence of actions that brings the agent back to the state just before this execution. It emerges, for example, if an agent needs to find out which action sequences are undoable, and which ones are committed choices. A prototypical scenario is in the context of plan execution in a nondeterministic environment: Upon detecting that after executing some steps of the plan, an unintended state has been reached, backtracking to an earlier state by taking appropriate undo actions can be useful for recovery. In this paper, we consider the problem of undoing the effects of an action sequence by means of a reverse plan. Intuitively, by executing a reverse plan for an action sequence AS at the state reached after AS, the agent can always reach the state S she was at just before executing AS, possibly subject to conditions on the current state and S. Notably, this problem is different from a vanilla planning problem, since the state we have to get back to is in general unknown. We study this problem in a general logic-based action representation framework that can accommodate nondeterminism and concurrency. We formally define the notion of a reverse plan and determine the computational complexity of the existence and the recognition of such a plan. Guided by these results, we then present algorithms for constructing reverse plans. Unsurprisingly, the problem is intractable in general, and we present a knowledge compilation approach that constructs offline a reverse plan library for efficient (in some cases, linear time) online computation of action reversals. Our results for the generic framework can be adapted for expressive action languages such as or . [Copyright &y& Elsevier]

Abstract: Traditionally, consistency is the only criterion for the quality of a theory in logic-based approaches to reasoning about actions. This work goes beyond that and contributes to the metatheory of actions by investigating what other properties a good domain description should have. We state some metatheoretical postulates concerning this sore spot. When all postulates are satisfied we call the action theory modular. Besides being easier to understand and more elaboration tolerant in McCarthy''s sense, modular theories have interesting properties. We point out the problems that arise when the postulates about modularity are violated, and propose algorithmic checks that can help the designer of an action theory to overcome them. [Copyright &y& Elsevier]

Consider an agent executing a plan with nondeterministic actions, in a dynamic environment, which might fail. Suppose that she is given a description of this action domain, including specifications of effects of actions, and a set of trajectories for the execution of this plan, where each trajectory specifies a possible execution of the plan in this domain. After executing some part of the plan, suppose that she obtains information about the current state of the world, and notices that she is not at a correct state relative to the given trajectories. How can she find an explanation (a point of failure) for such a discrepancy? An answer to this question can be useful for different purposes. In the context of execution monitoring, points of failure can determine some checkpoints that specify when to check for discrepancies, and they can sometimes be used for recovering from discrepancies that cause plan failures. At the modeling level, points of failure may provide useful insight into the action domain for a better understanding of the domain, or reveal errors in the formalization of the domain. We study the question above in a general logic-based knowledge representation framework, which can accommodate nondeterminism and concurrency. In this framework, we define a discrepancy and an explanation for it, and analyze the computational complexity of detecting discrepancies and finding explanations for them. We introduce a method for computing explanations, and report about a realization of this method using DLV^K, which is a logic-programming based system for reasoning about actions and change. [ABSTRACT FROM AUTHOR]

Abstract: This work faces the problem of automatic selection and composition of web services, discussing the advantages that derive from the inclusion, in a web service declarative description, of the high-level communication protocol, that is used by the service for interacting with its partners, allowing a rational inspection of it. The approach we propose is set in the Semantic Web field of research and inherits from research in the field of multi-agent systems. Web services are viewed as software agents, communicating by predefined sharable interaction protocols. A logic programming framework based on modal logic is proposed, where the protocol-based interactions of web services are formalized and the use of reasoning about actions and change techniques (planning) for performing the tasks of selection and composition of web services in a way that is personalized w.r.t. the user request is enabled. We claim that applying reasoning techniques on a declarative specification of the service interactions allows to gain flexibility in fulfilling the user preference in the context of a web service matchmaking process. [Copyright &y& Elsevier]

In this article we consider three different kinds of domain-dependent control knowledge (temporal, procedural and HTN-based) that are useful in planning. Our approach is declarative and relies on the language of logic programming with answer set semantics (AnsProlog). AnsProlog is designed to plan without control knowledge. We show how temporal, procedural and HTN-based control knowledge can be incorporated into AnsProlog by the modular addition of a small number of domain-dependent rules, without the need to modify the planner. We formally prove the correctness of our planner, both in the absence and presence of the control knowledge. Finally, we perform some initial experimentation that demonstrates the potential reduction in planning time that can be achieved when procedural domain knowledge is used to solve planning problems with large plan length. [ABSTRACT FROM AUTHOR]

The first step in reasoning about actions and change involves reasoning about how the world would evolve if a certain action is executed in a certain state. Most research on this assumes the evolution to be only a single step and focus on formulating the transition function that defines changes between states due to actions. In this paper we consider cases where the evolution is more than just a single change between one state and another. This is manifested when the execution of an action may trigger execution of other actions, or when multiple agents act on the environment following certain strategies. [ABSTRACT FROM AUTHOR]

In this paper we describe an approach to the construction of adaptive tutoring systems, based on techniques from the research area of Reasoning about Actions and Change.This approach leads to the implementation of a prototype system, having a multi-agent architecture, whose kernel is a set of rational agents, programmed in the logic programming language DyLOG. In the prototype that we implemented the reasoning capabilities of the agents are exploited both to dynamically build study plans and to verify the correctness of user-given study plans with respect to the competence that the user wants to acquire. [ABSTRACT FROM AUTHOR]

The nonmonotonic causal logic defined in this paper can be used to represent properties of actions, including actions with conditional and indirect effects, nondeterministic actions, and concurrently executed actions. It has been applied to several challenge problems in the theory of commonsense knowledge. We study the relationship between this formalism and other work on nonmonotonic reasoning and knowledge representation, and discuss its implementation, called the Causal Calculator. [Copyright &y& Elsevier]

The work described in this report is motivated by the desire to test the expressive possibilities of action language C+. The Causal Calculator (CCalc) is a system that answers queries about action domains described in a fragment of that language. The Zoo World and the Traffic World have been proposed by Erik Sandewall in his Logic Modelling Workshop—an environment for communicating axiomatizations of action domains of nontrivial size.The Zoo World consists of several cages and the exterior, gates between them, and animals of several species, including humans. Actions in this domain include moving within and between cages, opening and closing gates, and mounting and riding animals. The Traffic World includes vehicles moving continuously between road crossings subject to a number of restrictions, such as speed limits and keeping a fixed safety distance away from other vehicles on the road. We show how to represent the two domains in the input language of CCalc, and how to use CCalc to test these representations. [Copyright &y& Elsevier]

We propose the action language EPEC – Epistemic Probabilistic Event Calculus – that supports probabilistic, epistemic reasoning about narratives of action occurrences and environmentally triggered events, and in particular facilitates reasoning about future belief-conditioned actions and their consequences in domains that include both perfect and imperfect sensing actions. To provide a declarative semantics for sensing and belief conditioned actions in a probabilistic, narrative setting we introduce the novel concept of an epistemic reduct. We then formally compare our language with two established frameworks for probabilistic reasoning about action – the action language PAL by Baral et al., and the extension of the situation calculus to reason about noisy sensors and effectors by Bacchus et al. In both cases we prove a correspondence with EPEC for a class of domains representable in both frameworks. [ABSTRACT FROM AUTHOR]

In this paper we consider how the three main approaches to ethics – deontology, consequentialism and virtue ethics – relate to the implementation of ethical agents. We provide a description of each approach and how agents might be implemented by designers following the different approaches. Although there are numerous examples of agents implemented within the consequentialist and deontological approaches, this is not so for virtue ethics. We therefore propose a novel means of implementing agents within the virtue ethics approach. It is seen that each approach has its own particular strengths and weaknesses when considered as the basis for implementing ethical agents, and that the different approaches are appropriate to different kinds of system. [ABSTRACT FROM AUTHOR]