Logic & Formal Reasoning
Reasoning for Moving Blocks Problem: Formal Representation and Implementation
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.
Online Inference-Rule Learning from Natural-Language Extractions
Raghavan, Sindhu (The University of Texas at Austin) | Mooney, Raymond J. (The University of Texas at Austin)
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.
Progression of Decomposed Situation Calculus Theories
Ponomaryov, Denis (University of Ulm) | Soutchanski, Mikhail (Ryerson University)
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.
Learning Guided Planning for Robust Task Execution in Cognitive Robotics
Karapinar, Sertac (Istanbul Technical University) | Sariel-Talay, Sanem (Istanbul Technical University) | Yildiz, Petek (Istanbul Technical University) | Ersen, Mustafa (Istanbul Technical University)
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.
Procedural Approach to Mitigating Concurrently Applied Clinical Practice Guidelines
Michalowski, Martin (Adventium Labs) | Wilk, Szymon (Poznan University of Technology) | Michalowski, Wojtek (University of Ottawa) | Tan, Xing (University of Ottawa) | Lin, Di (McGill University) | Mohapatra, Subhra (University of Ottawa)
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.
Backdoors to Tractability of Answer-Set Programming
Fichte, Johannes Klaus (Vienna University of Technology)
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.
A First-Order Logic Based Framework for Verifying Simulations
Nyew, Hui Meen (Michigan Technological University) | Onder, Nilufer (Michigan Technological University) | Onder, Soner (Michigan Technological University) | Wang, Zhenlin (Michigan Technological University)
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.
Filtering With Logic Programs and Its Application to General Game Playing
Thielscher, Michael (The University of New South Wales)
Motivated by the problem of building a basic reasoner for general game playing with imperfect information, we address the problem of filtering with logic programs, whereby an agent updates its incomplete knowledge of a program by observations. We develop a filtering method by adapting an existing backward-chaining and abduction method for so-called open logic programs. Experimental results show that this provides a basic effective and efficient "legal" player for general imperfect-information games.
Partial MUS Enumeration
Previti, Alessandro (University College Dublin) | Marques-Silva, Joao (University College Dublin)
Minimal explanations of infeasibility find a wide range of uses. In the Boolean domain, these are referred to as Minimal Unsatisfiable Subsets (MUSes). In some settings, one needs to enumerate MUSes of a Boolean formula. Most often the goal is to enumerate all MUSes. In cases where this is computationally infeasible, an alternative is to enumerate some MUSes. This paper develops a novel approach for partial enumeration of MUSes, that complements existing alternatives. If the enumeration of all MUSes is viable, then existing alternatives represent the best option. However, for formulas where the enumeration of all MUSes is unrealistic, our approach provides a solution for enumerating some MUSes within a given time bound. The experimental results focus on formulas for which existing solutions are unable to enumerate MUSes, and shows that the new approach can in most cases enumerate a non-negligible number of MUSes within a given time bound.