Goto

Collaborating Authors

 Logic & Formal Reasoning


Causal Learnability

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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

AAAI Conferences

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.