Logic & Formal Reasoning
Inference in Probabilistic Logic Programs using Weighted CNF's
Fierens, Daan, Broeck, Guy Van den, Thon, Ingo, Gutmann, Bernd, De Raedt, Luc
Probabilistic logic programs are logic programs in which some of the facts are annotated with probabilities. Several classical probabilistic inference tasks (such as MAP and computing marginals) have not yet received a lot of attention for this formalism. The contribution of this paper is that we develop efficient inference algorithms for these tasks. This is based on a conversion of the probabilistic logic program and the query and evidence to a weighted CNF formula. This allows us to reduce the inference tasks to well-studied tasks such as weighted model counting. To solve such tasks, we employ state-of-the-art methods. We consider multiple methods for the conversion of the programs as well as for inference on the weighted CNF. The resulting approach is evaluated experimentally and shown to improve upon the state-of-the-art in probabilistic logic programming.
On Unit-Refutation Complete Formulae with Existentially Quantified Variables
Bordeaux, Lucas (Microsoft Research, Cambridge) | Janota, Mikolas (INESC-ID, Lisboa) | Marques-Silva, Joao (University College Dublin) | Marquis, Pierre (CRIL-CNRS, University of Artois)
We analyze, along the lines of the knowledge compilation map, both the tractability and the succinctness of the propositional language URC of unit-refutation complete propositional formulae, as well as its disjunctive closure URC[V, ∃], and a superset of URC where variables can be existentially quantified and unit-refutation completeness concerns only consequences built up from free variables.
Fixed-Parameter Algorithms for Finding Minimal Models
Lackner, Martin (Vienna University of Technology) | Pfandler, Andreas (Vienna University of Technology)
Computing minimal models is an important task in Knowledge Representation and Reasoning that appears in formalisms such as circumscription, diagnosis and answer set programming. Even the most basic question of whether there exists a minimal model containing a given variable is known to be $\Sigma_2^P$-complete. In this work we study the problem of computing minimal models from the viewpoint of parameterized complexity theory. We perform an extensive complexity analysis of this problem with respect to eleven parameters. Tractable fragments based on combinations of these parameters are identified by giving several fixed-parameter algorithms. For the remaining combinations we show parameterized hardness results and thus prove that under usual complexity theoretic assumptions no further fixed-parameter algorithms exist for these parameters.
Strong Equivalence of Qualitative Optimization Problems
Faber, Wolfgang (University of Calabria) | Truszczyński, Mirosław (University of Kentucky) | Woltran, Stefan (Vienna University of Technology)
We introduce the framework of qualitative optimization problems (or, simply, optimization problems) to represent preference theories. The formalism uses separate modules to describe the space of outcomes to be compared (the generator) and the preferences on outcomes (the selector). We consider two types of optimization problems. They differ in the way the generator, which we model by a propositional theory, is interpreted: by the standard propositional logic semantics, and by the equilibrium-model (answer-set) semantics. Under the latter interpretation of generators, optimization problems directly generalize answer-set optimization programs proposed previously. We study strong equivalence of optimization problems, which guarantees their interchangeability within any larger context. We characterize several versions of strong equivalence obtained by restricting the class of optimization problems that can be used as extensions and establish the complexity of associated reasoning tasks. Understanding strong equivalence is essential for modular representation of optimization problems and rewriting techniques to simplify them without changing their inherent properties.
An Abstraction Technique for the Verification of Artifact-Centric Systems
Belardinelli, Francesco (Imperial College London) | Lomuscio, Alessio (Imperial College London) | Patrizi, Fabio (Sapienza Universita')
We explore the paradigm of artifact-centric systems from a knowledge-based perspective. We provide a semantics based on interpreted-systems to interpret a first-order temporal- epistemic language with identity in a multi-agent setting. We consider the model checking problem for this language and provide abstraction results. We isolate a natural subclass of artifact-systems for which the model checking problem is decidable. We give an upper bound on the complexity of the model checking problem.
Rewriting Ontological Queries into Small Nonrecursive Datalog Programs
Gottlob, Georg (University of Oxford) | Schwentick, Thomas (TU Dortmund University)
We consider the setting of ontological database access, where an A-box is given in form of a relational database D and where a Boolean conjunctive query q has to be evaluated against D modulo a T-box Σ formulated in DL-Lite or Linear Datalog+/-. It is well-known that (Σ, q) can be rewritten into an equivalent nonrecursive Datalog program P that can be directly evaluated over D. However, for Linear Datalog+/- or for DL-Lite versions that allow for role inclusion, the rewriting methods described so far result in a nonrecursive Datalog program P of size exponential in the joint size of Σ and q . This gives rise to the interesting question whether such a rewriting necessarily needs to be of exponential size. In this paper we show that it is actually possible to translate (Σ, q ) into a polynomially sized equivalent nonrecursive Datalog program P.
Ordered Epistemic Logic: Semantics, Complexity and Applications
Vlaeminck, Hanne (Katholieke Universiteit Leuven) | Vennekens, Joost (Katholieke Universiteit Leuven) | Bruynooghe, Maurice (Katholieke Universiteit Leuven) | Denecker, Marc (Katholieke Universiteit Leuven)
Many examples of epistemic reasoning in the literature exhibit a stratified structure: defaults are formulated on top of an incomplete knowledge base. These defaults derive extra information in case information is missing in the knowledge base. In autoepistemic logic, default logic and ASP this inherent stratification is not preserved as they may refer to their own knowledge or logical consequences. Defining the semantics of such logics requires a complex mathematical construction. As an alternative, this paper further develops ordered epistemic logic. This logic extends first order logic with a modal operator and stratification is maintained. This allows us to define an easy to understand semantics. Moreover, inference tasks have a lower complexity than in autoepistemic logic and the logic integrates seamlessly into classical logic and its extensions. In this paper we also propose a generalization of ordered epistemic logic, which we call distributed ordered epistemic logic. We argue that it can provide a semantic foundation for a number of distributed knowledge representation formalisms found in the literature.
Declarative Entity Resolution via Matching Dependencies and Answer Set Programs
Bahmani, Zeinab (Carleton University) | Bertossi, Leopoldo (Carleton University) | Kolahi, Solmaz (University of British Columbia) | Lakshmanan, Laks V. S. (University of British Columbia)
Entity resolution (ER) is an important and common problem in data cleaning. It is about identifying and merging records in a database that represent the same real-world entity. Recently, matching dependencies (MDs) have been introduced and investigated as declarative rules that specify ER. An ER process induced by MDs over a dirty instance leads to multiple clean instances, in general. In this work, we present disjunctive answer set programs (with stable model semantics) that capture through their models the class of alternative clean instances obtained after an ER process based on MDs. With these programs, we can obtain clean answers to queries, i.e. those that are invariant under the clean instances, by skeptically reasoning from the program. We investigate the ER programs in terms of expressive power for the ER task at hand. As an important special and practical case of ER, we provide a declarative reconstruction of the so-called union-case ER methodology, as presented through a generic approach to ER (the so-called Swoosh approach).
Temporal Composite Actions with Constraints
Doherty, Patrick (Linköping University) | Kvarnström, Jonas (Linköping University) | Szalas, Andrzej (Warzaw University)
Complex mission or task specification languages play a fundamentally important role in human/robotic interaction. In realistic scenarios such as emergency response, specifying temporal, resource and other constraints on a mission is an essential component due to the dynamic and contingent nature of the operational environments. It is also desirable that in addition to having a formal semantics, the language should be sufficiently expressive, pragmatic and abstract. The main goal of this paper is to propose a mission specification language that meets these requirements. It is based on extending both the syntax and semantics of a well-established formalism for reasoning about action and change, Temporal Action Logic (TAL), in order to represent temporal composite actions with constraints. Fixpoints are required to specify loops and recursion in the extended language. The results include a sound and complete proof theory for this extension. To ensure that the composite language constructs are adequately grounded in the pragmatic operation of robotic systems, Task Specification Trees (TSTs) and their mapping to these constructs are proposed. The expressive and pragmatic adequacy of this approach is demonstrated using an emergency response scenario.
Complexity-Sensitive Decision Procedures for Abstract Argumentation
Dvorak, Wolfgang (Vienna University of Technology) | Järvisalo, Matti (University of Helsinki) | Wallner, Johannes Peter (Vienna University of Technology) | Woltran, Stefan (Vienna University of Technology)
Abstract argumentation frameworks (AFs) provide the basis for various reasoning problems in the areas of Knowledge Representation and Artificial Intelligence. Efficient evaluation of AFs has thus been identified as an important research challenge. So far, implemented systems for evaluating AFs have either followed a straight-forward reduction-based approach or been limited to certain tractable classes of AFs. In this work, we present a generic approach for reasoning over AFs, based on the novel concept of complexity-sensitivity. Establishing the theoretical foundations of this approach, we derive several new complexity results for preferred, semistable and stage semantics which complement the current complexity landscape for abstract argumentation, providing further understanding on the sources of intractability of AF reasoning problems. The introduced generic framework exploits decision procedures for problems of lower complexity whenever possible. This allows, in particular, instantiations of the generic framework via harnessing in an iterative way current sophisticated Boolean satisfiability (SAT) solver technology for solving the considered AF reasoning problems. First experimental results show that the SAT-based instantiation of our novel approach outperforms existing systems.