Recently there has been an increasing interest in incorporating "intensional" functions in answer set programming. Intensional functions are those whose values can be described by other functions and predicates, rather than being pre-defined as in the standard answer set programming. We demonstrate that the functional stable model semantics plays an important role in the framework of "Answer Set Programming Modulo Theories (ASPMT)" — a tight integration of answer set programming and satisfiability modulo theories, under which existing integration approaches can be viewed as special cases where the role of functions is limited. We show that "tight" ASPMT programs can be translated into SMT instances, which is similar to the known relationship between ASP and SAT.

We present ReAct!, an interactive tool for high-level reasoning for cognitive robotic applications. ReAct! enables robotic researchers to describe robots' actions and change in dynamic domains, without having to know about the syntactic and semantic details of the underlying formalism in advance, and solve planning problems using state-of-the-art automated reasoners, without having to learn about their input/output language or usage. In particular, ReAct! can be used to represent sophisticated dynamic domains that feature concurrency, indirect effects of actions, and state/transition constraints. It allows for embedding externally defined calculations (e.g., checking for collision-free continuous trajectories) into representations of hybrid domains that require a tight integration of (discrete) high-level reasoning with (continuous) geometric reasoning. ReAct! also enables users to solve planning problems that involve complex goals. Such variety of utilities are useful for robotic researchers to work on interesting and challenging domains, ranging from service robotics to cognitive factories. ReAct! provides sample formalizations of some action domains (e.g., multi-agent path planning, Tower of Hanoi), as well as dynamic simulations of plans computed by a state-of-the-art automated reasoner (e.g., a SAT solver or an ASP solver).

The combined approach of the Qualitative Reasoning and Probabilistic Functions for the knowledge representation is proposed. The method aims at represent uncertain, qualitative knowledge that is essential for the moving blocks task's execution. The attempt to formalize the commonsense knowledge is performed with the Situation Calculus language for reasoning and robot's beliefs representation. The method is implemented in the Prolog programming language and tested for a specific simulated scenario. In most cases the implementation enables us to solve a given task, i.e., move blocks to desired positions. The example of robot's reasoning and main parts of the implemented program's code are presented.

In this paper, we consider the problem of learning commonsenseknowledge in the form of first-order rules from incomplete and noisynatural-language extractions produced by an off-the-shelf informationextraction (IE) system. Much of the information conveyed in text mustbe inferred from what is explicitly stated since easily inferablefacts are rarely mentioned. The proposed rule learner accounts forthis phenomenon by learning rules in which the body of the rulecontains relations that are usually explicitly stated, while the heademploys a less-frequently mentioned relation that is easilyinferred. The rule learner processes training examples in an onlinemanner to allow it to scale to large text corpora. Furthermore, wepropose a novel approach to weighting rules using a curated lexicalontology like WordNet. The learned rules along with their parametersare then used to infer implicit information using a Bayesian LogicProgram. Experimental evaluation on a machine reading testbeddemonstrates the efficacy of the proposed methods.

In many tasks related to reasoning about consequences of a logical theory, it is desirable to decompose the theory into a number of components with weakly-related or independent signatures. This facilitates reasoning when signature of a query formula belongs to only one of the components. However, an initial theory may be subject to change due to execution of actions affecting features mentioned in the theory. Having once computed a decomposition of a theory, one would like to know whether a decomposition has to be computed again for the theory obtained from taking into account the changes resulting from execution of an action. In the paper, we address this problem in the scope of the situation calculus, where change of an initial theory is related to the well-studied notion of progression. Progression provides a form of forward reasoning; it relies on forgetting values of those features which are subject to change and computing new values for them. We prove new results about properties of decomposition components under forgetting and show when a decomposition can be preserved in progression of an initial theory.

Modularity is essential for modeling large-scale practical applications. We propose modular logic programs as a modular version of answer set programming and study the relationship of our formalism to an earlier concept of lp-modules.

A cognitive robot may face failures during the execution of its actions in the physical world. In this paper, we investigate how robots can ensure robustness by gaining experience on action executions, and we propose a lifelong experimental learning method. We use Inductive Logic Programming (ILP) as the learning method to frame new hypotheses. ILP provides first-order logic representations of the derived hypotheses that are useful for reasoning and planning processes. Furthermore, it can use background knowledge to represent more advanced rules. Partially specified world states can also be easily represented in these rules. All these advantages of ILP make this approach superior to attribute-based learning approaches. Experience gained through incremental learning is used as a guide to future decisions of the robot for robust execution. The results on our Pioneer 3DX robot reveal that the hypotheses framed for failure cases are sound and ensure safety in future tasks of the robot.

There is a pressing need in clinical practice to mitigate (identify and address) adverse interactions that occur when a comorbid patient is managed according to multiple concurrently applied disease-specific clinical practice guidelines (CPGs). We describe an automatic algorithm for mitigating undesirable interactions for pairs of CPGs. The algorithm constructs logical models of processed CPGs and employs constraint logic programming to solve them. It handles two important issues frequently occurring in CPGs - iterative actions forming a cycle and numerical measurements. Dealing with these two issues in practice relies on a physician's knowledge and the manual analysis of CPGs. Yet for guidelines to be considered stand-alone and an easy to use clinical decision support tool this process needs to be automated. In this paper we present our algorithm that aims to build such a tool by mitigating multiple CPGs while handling cycles and numerical measurements. The application of the mitigation algorithm is illustrated with a clinical case study involving a comorbid patient suffering from atrial fibrillation in the setting of Wolff-Parkinsons-White syndrome.

The practical results of answer-set programming indicate that classical complexity theory is insufficient as a theoretical framework to explain why modern answer-set programming solvers work fast on industrial applications. Complexity analysis by means of parameterized complexity theory seems to be promising, because we think that the reason for the gap between theory and practice is the presence of a "hidden structure" in real-world instances. The application of parameterized complexity theory to answer-set programming would give a crucial understanding of how solver heuristics work. This profound understanding can be used to improve the decision heuristics of modern solvers and yields new efficient algorithms for decision problems in the nonmonotonic setting. My research aims to explain the gap between theoretical upper bounds and the effort to solve real-world instances. I will further develop by means of parameterized complexity exact algorithms which work efficiently for real-world instances. The approach is based on backdoors which are small sets of atoms that represent "clever reasoning shortcuts" through the search space. The concept of backdoors is widely used in the areas of propositional satisfiability and constraint satisfaction. I will show how this concept can be adapted to the nonmonotonic setting and how it can be utilized to improve common algorithms.

Modern science relies on simulation techniques for understanding phenomenon, exploring design options, or evaluating models. Assuring the correctness of simulators is a key problem where a multitude of solutions ranging from manual inspection to formal verification are applicable. Formal verification incorporates the rigor necessary but not all simulators are generated from formal specifications. Manual inspection is readily available but lacks the rigor and is prone to errors. In this paper, we describe an automated verification system (AVS) where the constraints that the system must adhere to are specified by the user in general purpose first-order logic. AVS translates these constraints into a verification program that scans the simulator traceand verifies that no constraints are violated. Computer microarchitecture simulations were successfully used to demonstrate the proposed approach. This paper describes the preliminary results and discusses how artificial intelligence techniques can be used to facilitate effective run-time verification of simulators.