Logic & Formal Reasoning
Causal Learnability
Michael, Loizos (Open University of Cyprus)
The ability to predict, or at least recognize, the state of the world that an action brings about, is a central feature of autonomous agents. We propose, herein, a formal framework within which we investigate whether this ability can be autonomously learned. The framework makes explicit certain premises that we contend are central in such a learning task: (i) slow sensors may prevent the sensing of an action's direct effects during learning; (ii) predictions need to be made reliably in future and novel situations. We initiate in this work a thorough investigation of the conditions under which learning is or is not feasible. Despite the very strong negative learnability results that we obtain, we also identify interesting special cases where learning is feasible and useful.
Existential Closures for Knowledge Compilation
Marquis, Pierre (CRIL-CNRS and Université)
We study the existential closures of several propositional languages L considered recently as target languages for knowledge compilation (KC), namely the incomplete fragments KROM-C, HORN-C, K/H-C, renH-C, AFF, and the corresponding disjunction closures KROM-C[V], HORN-C[V], K/H-C[V], renH-C[V], and AFF[V]. We analyze the queries, transformations, expressiveness and succinctness of the resulting languages L[E] in order to locate them in the KC map. As a by-product, we also address several issues concerning disjunction closures that were left open so far. From our investigation, the language HORN-C[V, E] (where disjunctions and existential quantifications can be applied to Horn CNF formulae) appears as an interesting target language for the KC purpose, challenging the influential DNNF languages.
Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics
Lutz, Carsten (Universitaet Bremen) | Wolter, Frank (University of Liverpool)
We study uniform interpolation and forgetting in the description logic ALC. Our main results are model-theoretic characterizations of uniform interpolants and their existence in terms of bisimulations, tight complexity bounds for deciding the existence of uniform interpolants, an approach to computing interpolants when they exist, and tight bounds on their size. We use a mix of model-theoretic and automata-theoretic methods that, as a by-product, also provides charachterizations of, and decision procedures for, conservative extensions.
On the Progression of Knowledge in the Situation Calculus
Liu, Yongmei (Sun Yat-sen University) | Wen, Ximing (Sun Yat-sen University and Guangdong Institute of Public Administration)
In a seminal paper, Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. Earlier works by Moore, Scherl and Levesque extended the situation calculus to account for knowledge. In this paper, we study progression of knowledge in the situation calculus. We first adapt the concept of bisimulation from modal logic and extend Lin and Reiter's notion of progression to accommodate knowledge. We show that for physical actions, progression of knowledge reduces to forgetting predicates in first-order modal logic. We identify a class of first-order modal formulas for which forgetting an atom is definable in first-order modal logic. This class of formulas goes beyond formulas without quantifying-in. We also identify a simple case where forgetting a predicate reduces to forgetting a finite number of atoms. Thus we are able to show that for local-effect physical actions, when the initial KB is a formula in this class, progression of knowledge is definable in first-order modal logic. Finally, we extend our results to the multi-agent case.
Logic Programming for Boolean Networks
Inoue, Katsumi (National Institute of Informatics)
The Boolean network is a mathematical model of biological systems, and has attracted much attention as a qualitative tool for analyzing the regulatory system. The stable states and dynamics of Boolean networks are characterized by their attractors, whose properties have been analyzed computationally, yet not much work has been done from the viewpoint of logical inference systems. In this paper, we show direct translations of Boolean networks into logic programs, and propose new methods to compute their trajectories and attractors based on inference on such logic programs. In particular, point attractors of both synchronous and asynchronous Boolean networks are characterized as supported models of logic programs so that SAT techniques can be applied to compute them. Investigation of these relationships suggests us to view Boolean networks as logic programs and vice versa.
Generalising the Interaction Rules in Probabilistic Logic
Hommersom, Arjen (Radboud University Nijmegen) | Lucas, Peter J. F. (Radboud University Nijmegen)
Probabilistic logics which is followed by the development of the main methods that support reasoning with probability distributions, used in generalising probabilistic Boolean interaction, and, such as ProbLog, use an implicit definition finally, default logic is briefly discussed. We will use probabilistic of an interaction rule to combine probabilistic evidence Boolean interaction as a sound and generic, algebraic about atoms. In this paper, we show that way to combine uncertain evidence, whereas default this interaction rule is an example of a more general logic will be used as our language to implement the interaction class of interactions that can be described by nonmonotonic operators, again reflecting this double perspective on the logics. We furthermore show that such probabilistic logic. The new probabilistic logical framework local interactions about the probability of an atom is described in Section 3 and compared to other approaches can be described by convolution. The resulting extended in Section 4. The achievements of this research are reflected probabilistic logic supports nonmonotonic upon in Section 5. reasoning with probabilistic information.
Belief Management for High-Level Robot Programs
Gspandl, Stephan (Graz University of Technology) | Pill, Ingo (Graz University of Technology) | Reip, Michael (Graz University of Technology) | Steinbauer, Gerald (Graz University of Technology) | Ferrein, Alexander (RWTH Aachen University)
The robot programming and plan language IndiGolog allows for on-line execution of actions and offline projections of programs in dynamic and partly unknown environments. Basic assumptions are that the outcomes of primitive and sensing actions are correctly modeled, and that the agent is informed about all exogenous events beyond its control. In real-world applications, however, such assumptions do not hold. In fact, an actionโs outcome is error-prone and sensing results are noisy. In this paper, we present a belief management system in IndiGolog that is able to detect inconsistencies between a robotโs modeled belief and what happened in reality. The system furthermore derives explanations and maintains a consistent belief. Our main contributions are (1) a belief management system following a history-based diagnosis approach that allows an agent to actively cope with faulty actions and the occurrence of exogenous events; and (2) an implementation in IndiGolog and experimental results from a delivery domain.
Succinctness of Epistemic Languages
French, Tim (The University of Western Australia) | Hoek, Wiebe van der (University of Liverpool) | Iliev, Petar (University of Liverpool) | Kooi, Barteld (University of Groningen)
Proving that one language is more succinct than another becomes harder when the underlying semantics is stronger. We propose to use Formula-Size Games (as put forward by Adler and Immerman, 2003), games that are played on two sets of models, and that directly link the length of play with the size of the formula. Using those games, we prove three succinctness results for m-dimensional modal logic: (1) In system K m , a notion of `everybody knows' makes the resulting language exponentially more succinct for m > 1, (2) In S5, the same language becomes more succinct for m > 3 and (3) Public Announcement Logic is exponentially more succinct than S5m, if m > 3. The latter settles an open problem raised by Lutz, 2006.
Fixpoints in Temporal Description Logics
Franconi, Enrico (Free University of Bozen-Bolzano) | Toman, David (University of Waterloo)
We study a decidable fixpoint extension of temporal description logics. To this end we employ and extend decidability results obtained for various temporally first-order monodic extensions of (first-order) description logics. Using these techniques we obtain decidability and tight complexity results for various fixpoint extensions of temporal description logics.
Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World
Fiorino, Guido (Università)
In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation.