Goto

Collaborating Authors

 Logic & Formal Reasoning


Inconsistency Management for Traffic Regulations

AAAI Conferences

Smart Cities is a vision driven by the availability of governmental data that fosters many challenging applications. One of them is the management of inconsistent traffic regulations, i.e., the handling of inconsistent traffic signs and measures in urban areas such as wrong sign posting, or errors in data acquisition in traffic sign administration software. We investigate such inconsistent traffic scenarios and formally model traffic regulations. Based on this, we consider relevant reasoning tasks including consistency testing, diagnosis, and repair, and present an implementation of the these tasks using answer set programming. The results of this research may improve existing governmental software maintaining traffic regulations.


Action-Based Imperative Programming with YAGI

AAAI Conferences

Many tasks for autonomous agents or robots are best de- scribed by a specification of the environment and a specifi- cation of the available actions the agent or robot can perform. Combining such a specification with the possibility to imper- atively program a robot or agent is what we call the action- based imperative programming. One of the most successful such approaches is Golog. In this paper, we draft a proposal for a new robot program- ming language YAGI, which is based on the action-based imperative programming paradigm. Our goal is to design a small, portable stand-alone YAGI interpreter. We combine the benefits of a principled domain specification with a clean, small and simple programming language, which does not ex- ploit any side-effects from the implementation language. We discuss general requirements of action-based programming languages and outline YAGI, our action-based language ap- proach which particularly aims at embeddability.


Towards an Expressive Decidable Logical Action Theory

AAAI Conferences

In the area of reasoning about actions, one of the key computational problems is the projection problem: to find whether a given logical formula is true after performing a sequence of actions. This problem is undecidable in the general situation calculus; however, it is decidable in some fragments. We consider a fragment P of the situation calculus and Reiterโ€™s basic action theories (BAT) such that the projection problem can be reduced to the satisfiability problem in an expressive description logic ALCO(U) that includes nominals (O), the universal role (U), and constructs from the well-known logic ALC. It turns out that our fragment P is more expressive than previously explored description logic based fragments of the situation calculus. We explore some of the logical properties of our theories. In particular, we show that the projection problem can be solved using regression in the case where BATs include a general โ€œstaticโ€ TBox, i.e., an ontology that has no occurrences of fluents. Thus, we propose seamless integration of traditional ontologies with reasoning about actions. We also show that the projection problem can be solved using progression if all actions have only local effects on the fluents, i.e., in P, if one starts with an incomplete initial theory that can be transformed into an ALCO(U) concept, then its progression resulting from the execution of a ground action can still be expressed in the same language. Moreover, we show that for a broad class of incomplete initial theories progression can be computed efficiently.


Challenges in Learning Optimum Models for Complex First Order Activity Recognition Settings

AAAI Conferences

Non intrusive activity recognition systems typically read values from sensors deployed in an environment and combine them with user annotated activities to build a probabilistic model. Recently, features constructed from activity specific conjunctions of binary sensor values have been shown to improve the classification accuracy. Such systems employ greedy feature induction techniques to find the observation features and combine them with state transition distribution in a Hidden Markov Model or a Conditional Random Field. An exhaustive search for optimum features is infeasible in this exponential feature space. We have recently extended the rule ensemble learning using hierarchical kernels (RELHKL) framework, that learns a sparse set of simple features and their optimum weights, to structured output spaces for learning optimum observation features along with the transition features and their weights. The exponentially large space of conjunctions is handled efficiently by exploiting its hierarchical structure. Our experiments have shown good improvement over other approaches. Although such approaches solve propositional classification problems optimally, their first-order extension is non-trivial and is a challenging problem. In this paper, we discuss about the challenges involved in leveraging the RELHKL in structured output spaces approach to learn optimum features in complex first order activity recognition settings.


Reformulating Temporal Action Logics in Answer Set Programming

AAAI Conferences

Temporal Action Logics (TAL) is a class of temporal logics for reasoning about actions. We present a reformulation of TAL in Answer Set Programming (ASP), and discuss some synergies it brings. First, the reformulation provides a means to compute TAL using efficient answer set solvers. Second, TAL provides a structured high-level language for ASP (possibly with constraint solving). Third, the reformulation allows us to compute integration of TAL and ontologies using answer set solvers, and we illustrate its usefulness in the healthcare domain in the context of medical expert systems.


Equality-Friendly Well-Founded Semantics and Applications to Description Logics

AAAI Conferences

We tackle the problem of defining a well-founded semantics for Datalog rules with existentially quantified variables in their heads and negations in their bodies. In particular, we provide a well-founded semantics (WFS) for the recent Datalog+/- family of ontology languages, which covers several important description logics (DLs). To do so, we generalize Datalog+/- by non-stratified nonmonotonic negation in rule bodies, and we define a WFS for this generalization via guarded fixed-point logic. We refer to this approach as equality-friendly WFS, since it has the advantage that it does not make the unique name assumption (UNA); this brings it close to OWL and its profiles as well as typical DLs, which also do not make the UNA. We prove that for guarded Datalog+/- with negation under the equality-friendly WFS, conjunctive query answering is decidable, and we provide precise complexity results for this problem. From these results, we obtain precise definitions of the standard WFS extensions of EL and of members of the DL-Lite family, as well as corresponding complexity results for query answering.


Temporally Expressive Planning Based on Answer Set Programming with Constraints

AAAI Conferences

Recently, a new language AC(C) was proposed to integrate answer set programming (ASP) and constraint logic programming (CLP). In this paper, we show that temporally expressive planning problems in PDDL2.1 can be translated into AC(C) and solved using AC(C) solvers. Compared with existing approaches, the new approach puts less restrictions on the planning problems and is easy to extend with new features like PDDL axioms. It can also leverage the inference engine for AC(C) which has the potential to exploit the best reasoning mechanisms developed in the ASP, SAT and CP communities.


FLP Semantics Without Circular Justifications for General Logic Programs

AAAI Conferences

The FLP semantics presented by (Faber, Leone, and Pfeifer 2004) has been widely used to define answer sets, called FLP answer sets, for different types of logic programs such as logic programs with aggregates, description logic programs (dl-programs), Hex programs, and logic programs with first-order formulas (general logic programs). However, it was recently observed that the FLP semantics may produce unintuitive answer sets with circular justifications caused by self-supporting loops. In this paper, we address the circular justification problem for general logic programs by enhancing the FLP semantics with a level mapping formalism. In particular, we extend the Gelfond-Lifschitz three step definition of the standard answer set semantics from normal logic programs to general logic programs and define for general logic programs the first FLP semantics that is free of circular justifications. We call this FLP semantics the well-justified FLP semantics. This method naturally extends to general logic programs with additional constraints like aggregates, thus providing a unifying framework for defining the well-justified FLP semantics for various types of logic programs. When this method is applied to normal logic programs with aggregates, the well-justified FLP semantics agrees with the conditional satisfaction based semantics defined by (Son, Pontelli, and Tu 2007); and when applied to dl-programs, the semantics agrees with the strongly well-supported semantics defined by (Shen 2011).


Learning Games from Videos Guided by Descriptive Complexity

AAAI Conferences

In recent years, several systems have been proposed that learn the rules of a simple card or board game solely from visual demonstration. These systems were constructed for specific games and rely on substantial background knowledge. We introduce a general system for learning board game rules from videos and demonstrate it on several well-known games. The presented algorithm requires only a few demonstrations and minimal background knowledge, and, having learned the rules, automatically derives position evaluation functions and can play the learned games competitively. Our main technique is based on descriptive complexity, i.e. the logical means necessary to define a set of interest. We compute formulas defining allowed moves and final positions in a game in different logics and select the most adequate ones. We show that this method is well-suited for board games and there is strong theoretical evidence that it will generalize to other problems.


Synthesizing Strategies for Epistemic Goals by Epistemic Model Checking: An Application to Pursuit Evasion Games

AAAI Conferences

The paper identifies a special case in which the complex problem of synthesis from specifications in temporal-epistemic logic can be reduced to the simpler problem of model checking such specifications. An application is given of strategy synthesis in pursuit-evasion games, where one or more pursuers with incomplete information aim to discover theexistence of an evader. Experimental results are provided to evaluate the feasibility of the approach.