Logic & Formal Reasoning
Splitting an LPMLN Program
Wang, Bin (Southeast University) | Zhang, Zhizheng (Southeast University) | Xu, Hongxiang (Southeast University) | Shen, Jun (Southeast University)
The technique called splitting sets has been proven useful in simplifying the investigation of Answer Set Programming (ASP). In this paper, we investigate the splitting set theorem for LP MLN that is a new extension of ASP created by combining the ideas of ASP and Markov Logic Networks (MLN). Firstly, we extend the notion of splitting sets to LP MLN programs and present the splitting set theorem for LP MLN . Then, the use of the theorem for simplifying several LP MLN inference tasks is illustrated. After that, we give two parallel approaches for solving LP MLN programs via using the theorem. The preliminary experimental results show that these approaches are alternative ways to promote an LP MLN solver.
Measuring Strong Inconsistency
Ulbricht, Markus (Leipzig University) | Thimm, Matthias (University Koblenz-Landau) | Brewka, Gerhard (Leipzig University)
We address the issue of quantitatively assessing the severity of inconsistencies in nonmonotonic frameworks. While measuring inconsistency in classical logics has been investigated for some time now, taking the nonmonotonicity into account poses new challenges. In order to tackle them, we focus on the structure of minimal strongly kb-inconsistent subsets of a knowledge base kb---a generalization of minimal inconsistency to arbitrary, possibly nonmonotonic, frameworks. We propose measures based on this notion and investigate their behavior in a nonmonotonic setting by revisiting existing rationality postulates, analyzing the compliance of the proposed measures with these postulates, and by investigating their computational complexity.
Visual Explanation by High-Level Abduction: On Answer-Set Programming Driven Reasoning About Moving Objects
Suchan, Jakob (University of Bremen) | Bhatt, Mehul (University of Bremen) | Waลega, Przemysลaw (รrebro University, Sweden) | Schultz, Carl (University of Warsaw)
We propose a hybrid architecture for systematically computing robust visual explanation(s) encompassing hypothesis formation, belief revision, and default reasoning with video data. The architecture consists of two tightly integrated synergistic components: (1) (functional) answer set programming based abductive reasoning with space-time tracklets as native entities; and (2) a visual processing pipeline for detection based object tracking and motion analysis. We present the formal framework, its general implementation as a (declarative) method in answer set programming, and an example application and evaluation based on two diverse video datasets: the MOTChallenge benchmark developed by the vision community, and a recently developed Movie Dataset.
Qualitative Reasoning About Cardinal Directions Using Answer Set Programming
Izmirlioglu, Yusuf (Sabanci University) | Erdem, Esra (Sabanci University)
In real world, the regions occupied by these entities may the location of an object, involve dealing with spatial properties have holes (e.g., Store A may have a small garden in the and relations of objects. For higher precision of solutions, middle) or may be disconnected (e.g., Store A may consist if data is available, quantitative approaches can be of two parts across a small street). Moreover, the given set of employed to find metric solutions for these tasks. On the constraints may be incomplete (i.e., qualitative spatial relations other hand, for some applications (e.g., exploration of an between some spatial objects are not known) or some unknown environment), quantitative data may not always be constraints may involve disjunctions (e.g., missing child is available due to incomplete knowledge about the environment; to the south of Store A or to the north of Store B). In such and, for some applications (e.g., that involve humanrobot cases, with uncertainty or incomplete knowledge, checking interactions) sociable and understandable interactions the consistency of a given set of constraints is NPcomplete and acceptable explanations are often more desirable than (Table 1).
Dependence in Propositional Logic: Formula-Formula Dependence and Formula Forgetting โ Application to Belief Update and Conservative Extension
Fang, Liangda (Jinan University) | Wan, Hai (Sun Yat-sen Univeristy) | Liu, Xianqiao (Sun Yat-sen University) | Fang, Biqing (Sun Yat-sen University) | Lai, Zhaorong (Jinan University)
Dependence is an important concept for many tasks in artificial intelligence. A task can be executed more efficiently by discarding something independent from the task. In this paper, we propose two novel notions of dependence in propositional logic: formula-formula dependence and formula forgetting. The first is a relation between formulas capturing whether a formula depends on another one, while the second is an operation that returns the strongest consequence independent of a formula. We also apply these two notions in two well-known issues: belief update and conservative extension. Firstly, we define a new update operator based on formula-formula dependence. Furthermore, we reduce conservative extension to formula forgetting.
Weighted Abstract Dialectical Frameworks
Brewka, Gerhard (Leipzig University) | Strass, Hannes (Leipzig University) | Wallner, Johannes P. (TU Wien) | Woltran, Stefan (TU Wien)
Abstract Dialectical Frameworks (ADFs) generalize Dung's argumentation frameworks allowing various relationships among arguments to be expressed in a systematic way. We further generalize ADFs so as to accommodate arbitrary acceptance degrees for the arguments. This makes ADFs applicable in domains where both the initial status of arguments and their relationship are only insufficiently specified by Boolean functions. We define all standard ADF semantics for the weighted case, including grounded, preferred and stable semantics. We illustrate our approach using acceptance degrees from the unit interval and show how other valuation structures can be integrated. In each case it is sufficient to specify how the generalized acceptance conditions are represented by formulas, and to specify the information ordering underlying the characteristic ADF operator. We also present complexity results for problems related to weighted ADFs.
Situation Calculus Semantics for Actual Causality
Batusov, Vitaliy (York University) | Soutchanski, Mikhail (Ryerson University)
The definitions of actual cause given by Pearl and Halpern (HP) in the framework of causal models provided vital computational insight into an old philosophical problem but by no means resolved it. One source of concern is the lack of objective criteria for selecting possible worlds to be admitted into the counterfactual analysis, epitomized by the competition between multiple proposals by HP and others. Another concern is due to the modest expressivity of propositional-level structural equations which limits their applicability and, arguably, contributes to the the former problem. We tackle both of these issues using a novel approach. We build our definition of actual cause from first principles in the context of atemporal situation calculus (SC) action theories with sequential actions. As a result, we can successfully identify actual causes of conditions expressed in first-order logic. We validate the HP approach by providing a formal translation from causal models to SC and proving a relationship between our definitions of actual cause and that of HP. Using well-known and new examples, we show that long-standing disagreements between alternative definitions of actual causality can be mitigated by faithful SC modelling of the domains.
Combining Rules and Ontologies into Clopen Knowledge Bases
Bajraktari, Labinot (TU Wien) | Ortiz, Magdalena (TU Wien) | ล imkus, Mantas (TU Wien)
We propose Clopen Knowledge Bases (CKBs) as a new formalism combining Answer Set Programming (ASP) with ontology languages based on first-order logic. CKBs generalize the prominent r-hybrid and DL+LOG languages of Rosati, and are more flexible for specification of problems that combine open-world and closed-world reasoning. We argue that the guarded negation fragment of first-order logic(GNFO)โa very expressive fragment that subsumes many prominent ontology languages like Description Logics (DLs) and the guarded fragmentโis an ontology language that can be used in CKBs while enjoying decidability for basic reasoning problems. We further show how CKBs can be used with expressive DLs of the ALC family, and obtain worst-case optimal complexity results in this setting. For DL-based CKBs, we define a fragment called separable CKBs (which still strictly subsumes r-hybrid and DL+LOG knowledge bases), and show that they can be rather efficiently translated into standard ASP programs. This approach allows us to perform basic inference from separable CKBs by reusing existing efficient ASP solvers. We have implemented the approach for separable CKBs containing ontologies in the DL ALCH, and present in this paper some promising empirical results for real-life data. They show that our approach provides a dramatic improvement over a naive implementation based on a translation of such CKBs into dl-programs.
Disjunctive Program Synthesis: A Robust Approach to Programming by Example
Raza, Mohammad (Microsoft Corporation) | Gulwani, Sumit (Microsoft Corporation)
Programming by example (PBE) systems allow end users to easily create programs by providing a few input-output examples to specify their intended task. The system attempts to generate a program in a domain specific language (DSL) that satisfies the given examples. However, a key challenge faced by existing PBE techniques is to ensure the robustness of the programs that are synthesized from a small number of examples, as these programs often fail when applied to new inputs. This is because there can be many possible programs satisfying a small number of examples, and the PBE system has to somehow rank between these candidates and choose the correct one without any further information from the user. In this work we present a different approach to PBE in which the system avoids making a ranking decision at the synthesis stage, by instead synthesizing a disjunctive program that includes the many top-ranked programs as possible alternatives and selects between these different choices upon execution on a new input. This delayed choice brings the important benefit of comparing the possible outputs produced by the different disjuncts on a given input at execution time. We present a generic framework for synthesizing such disjunctive programs in arbitrary DSLs, and describe two concrete implementations of disjunctive synthesis in the practical domains of data extraction from plain text and HTML documents. We present an evaluation showing the significant increase in robustness achieved with our disjunctive approach, as illustrated by an increase from 59% to 93% of tasks for which correct programs can be learnt from a single example.
Learning From Unannotated QA Pairs to Analogically Disambiguate and Answer Questions
Crouse, Maxwell (Northwestern University) | McFate, Clifton (Northwestern University) | Forbus, Kenneth (Northwestern University)
Creating systems that can learn to answer natural language questions has been a longstanding challenge for artificial intelligence. Most prior approaches focused on producing a specialized language system for a particular domain and dataset, and they required training on a large corpus manually annotated with logical forms. This paper introduces an analogy-based approach that instead adapts an existing general purpose semantic parser to answer questions in a novel domain by jointly learning disambiguation heuristics and query construction templates from purely textual question-answer pairs. Our technique uses possible semantic interpretations of the natural language questions and answers to constrain a query-generation procedure, producing cases during training that are subsequently reused via analogical retrieval and composed to answer test questions. Bootstrapping an existing semantic parser in this way significantly reduces the number of training examples needed to accurately answer questions. We demonstrate the efficacy of our technique using the Geoquery corpus, on which it approaches state of the art performance using 10-fold cross validation, shows little decrease in performance with 2-folds, and achieves above 50% accuracy with as few as 10 examples.