Logic & Formal Reasoning
A Syntax-Independent Approach to Forgetting in Disjunctive Logic Programs
Delgrande, James (Simon Fraser University) | Wang, Kewen (Griffith University)
A Forgetting is an operation for eliminating variables from a semantic theory of forgetting for normal logic programs knowledge base (Lin and Reiter 1994; Lang, Liberatore, and under answer set semantics is introduced in (Wang, Sattar, Marquis 2003). It constitutes a reduction in an agent's language and Su 2005), in which a sound and complete algorithm or, more accurately, the agent's signature. It has also is developed based on a series of program transformations; been studied under different names, such as variable elimination, this theory is further developed and extended uniform interpolation and relevance (Subramanian, to disjunctive logic programs in (Eiter and Wang 2006; Greiner, and Pearl 1997). Forgetting has various possible 2008). However, this theory of forgetting is defined in terms applications in a reasoning system. For example, in query of answer sets rather than SE models, and so again is not answering, if one can determine what is relevant to a query, syntax-independent.
asprin: Customizing Answer Set Preferences without a Headache
Brewka, Gerhard (University of Leipzig) | Delgrande, James (Simon Fraser University) | Romero, Javier (University of Potsdam) | Schaub, Torsten (University of Potsdam)
In this paper we describe asprin, a general, flexible, and extensible framework for handling preferences among the stable models of a logic program. We show how complex preference relations can be specified through user-defined preference types and their arguments. We describe how preference specifications are handled internally by so-called preference programs, which are used for dominance testing. We also give algorithms for computing one, or all, optimal stable models of a logic program. Notably, our algorithms depend on the complexity of the dominance tests and make use of multi-shot answer set solving technology.
Grounded Fixpoints
Bogaerts, Bart (KU Leuven) | Vennekens, Joost (KU Leuven) | Denecker, Marc (KU Leuven)
Algebraical fixpoint theory is an invaluable instrument for studying semantics of logics. For example, all major semantics of logic programming, autoepistemic logic, default logic and more recently, abstract argumentation have been shown to be induced by the different types of fixpoints defined in approximation fixpoint theory (AFT). In this paper, we add a new type of fixpoint to AFT: a grounded fixpoint of lattice operator O : L → L is defined as a lattice element x ∈ L such that O(x) = x and for all v ∈ L such that O(v ∧ x) ≤ v, it holds that x ≤ v. On the algebraical level, we show that all grounded fixpoints are minimal fixpoints approximated by the well-founded fixpoint and that all stable fixpoints are grounded. On the logical level, grounded fixpoints provide a new mathematically simple and compact type of semantics for any logic with a (possibly non-monotone) semantic operator. We explain the intuition underlying this semantics in the context of logic programming by pointing out that grounded fixpoints of the immediate consequence operator are interpretations that have no non-trivial unfounded sets. We also analyse the complexity of the induced semantics. Summarised, grounded fixpoint semantics is a new, probably the simplest and most compact, element in the family of semantics that capture basic intuitions and principles of various non-monotonic logics.
LARS: A Logic-Based Framework for Analyzing Reasoning over Streams
Beck, Harald (Vienna University of Technology) | Dao-Tran, Minh (Vienna University of Technology) | Eiter, Thomas (Vienna University of Technology) | Fink, Michael (Vienna University of Technology)
The recent rise of smart applications has drawn interest to logical reasoning over data streams. Different query languages and stream processing/reasoning engines were proposed. However, due to a lack of theoretical foundations, the expressivity and semantics of these diverse approaches were only informally discussed. Towards clear specifications and means for analytic study, a formal framework is needed to characterize their semantics in precise terms. We present LARS, a Logic-based framework for Analyzing Reasoning over Streams, i.e., a rule-based formalism with a novel window operator providing a flexible mechanism to represent views on streaming data. We establish complexity results for central reasoning tasks and show how the prominent Continuous Query Language (CQL) can be captured. Moreover, the relation between LARS and ETALIS, a system for complex event processing is discussed. We thus demonstrate the capability of LARS to serve as the desired formal foundation for expressing and analyzing different semantic approaches to stream processing/reasoning and engines.
Action Language BC+: Preliminary Report
Babb, Joseph (Arizona State University) | Lee, Joohyung (Arizona State University)
Action languages are formal models of parts of natural language that are designed to describe effects of actions. Many of these languages can be viewed as high level notations of answer set programs structured to represent transition systems. However, the form of answer set programs considered in the earlier work is quite limited in comparison with the modern Answer Set Programming (ASP) language, which allows several useful constructs for knowledge representation, such as choice rules, aggregates, and abstract constraint atoms. We propose a new action language called BC+, which closes the gap between action languages and the modern ASP language. Language BC+ is defined as a high level notation of propositional formulas under the stable model semantics. Due to the generality of the underlying language, BC+ is expressive enough to encompass many modern ASP language constructs and the best features of several other action languages, such as B, C, C+ and BC. Computational methods available in ASP solvers are readily applicable to compute BC+, which led us to implement the language by extending system Cplus2ASP.
Solving Distributed Constraint Optimization Problems Using Logic Programming
Le, Tiep (New Mexico State University) | Son, Tran Cao (New Mexico State University) | Pontelli, Enrico (New Mexico State University) | Yeoh, William (New Mexico State University)
This paper explores the use of answer set programming (ASP) in solving distributed constraint optimization problems (DCOPs). It makes the following contributions: (i)~It shows how one can formulate DCOPs as logic programs; (ii)~It introduces ASP-DPOP, the first DCOP algorithm that is based on logic programming; (iii)~It experimentally shows that ASP-DPOP can be up to two orders of magnitude faster than DPOP (its imperative-programming counterpart) as well as solve some problems that DPOP fails to solve due to memory limitations; and (iv)~It demonstrates the applicability of ASP in the wide array of multi-agent problems currently modeled as DCOPs.
Inference Graphs: Combining Natural Deduction and Subsumption Inference in a Concurrent Reasoner
Schlegel, Daniel R. (University at Buffalo) | Shapiro, Stuart C (University at Buffalo)
There are very few reasoners which combine natural deduction and subsumption reasoning, and there are none which do so while supporting concurrency. Inference Graphs are a graph-based inference mechanism using an expressive first-order logic, capable of subsumption and natural deduction reasoning using concurrency. Evaluation of concurrency characteristics on a combination natural deduction and subsumption reasoning problem has shown linear speedup with the number of processors.
Extending Analogical Generalization with Near-Misses
McLure, Matthew D. (Northwestern University) | Friedman, Scott E. (Smart Information Flow Technologies (SIFT)) | Forbus, Kenneth D. (Northwestern University)
Concept learning is a central problem for cognitive systems. Generalization techniques can help organize examples by their commonalities, but comparisons with non-examples, near-misses, can provide discrimination. Early work on near-misses required hand-selected examples by a teacher who understood the learner’s internal representations. This paper introduces Analogical Learning by Integrating Generalization and Near-misses (ALIGN) and describes three key advances. First, domain-general cognitive models of analogical processes are used to handle a wider range of examples. Second, ALIGN’s analogical generalization process constructs multiple probabilistic representations per concept via clustering, and hence can learn disjunctive concepts. Finally, ALIGN uses unsupervised analogical retrieval to find its own near-miss examples. We show that ALIGN out-performs analogical generalization on two perceptual data sets: (1) hand-drawn sketches; and (2) geospatial concepts from strategy-game maps.
Dialogue Understanding in a Logic of Action and Belief
Gabaldon, Alfredo (Carnegie Mellon University) | Langley, Pat (Carnegie Mellon University)
In recent work, Langley et al. (2014) introduced UMBRA, a systemfor plan and dialogue understanding. The program applies a form of abductive inference to generate explanations incrementally from relational descriptions of observed behavior and knowledge inthe form of rules. Although UMBRA's creators described the systemarchitecture, knowledge, and inferences, along with experimental studies of its operation, they did not provide a formalization of its structures or processes. In this paper, we analyze both aspects of the architecture in terms of the Situation Calculus — a classicallogic for reasoning about dynamical systems — and give a specification of the inference task the system performs. After this, we state some properties of this formalization thatare desirable for the task of incremental dialogue understanding. We conclude by discussing related work and describing our plans for additional research.
DynaDiffuse: A Dynamic Diffusion Model for Continuous Time Constrained Influence Maximization
Xie, Miao (University of Chinese Academy of Sciences) | Yang, Qiusong (Institute of Software, Chinese Academy of Sciences) | Wang, Qing (Institute of Software, Chinese Academy of Sciences) | Cong, Gao (Nanyang Technological University) | Melo, Gerard de (Tsinghua University/Microsoft Research Asia)
Studying the spread of phenomena in social networks is critical but still not fully solved. Existing influence maximization models assume a static network, disregarding its evolution over time. We introduce the continuous time constrained influence maximization problem for dynamic diffusion networks, based on a novel diffusion model called DynaDiffuse. Although the problem is NP-hard, the influence spread functions are monotonic and submodular, enabling fast approximations on top of an innovative stochastic model checking approach. Experiments on real social network data show that our model finds higher quality solutions and our algorithm outperforms state-of-art alternatives.