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.

However, it is well-known that applying machine learning and data mining to novel data sets is Finally, inspired by the field of constraint programming, challenging because each application imposes its own requirements (Guns et al. 2013) aim at developing declarative modeling and constraints that often require the development languages for specifying a wide range of mining problems. of new algorithms and systems. While there are software Such languages should support packages and tools such as Scikit for machine learning the high-level and natural modeling of pattern mining and Weka, Orange or Knime for data mining, adapting them tasks; that is, the models should closely correspond to to novel tasks is not easy, which explains why one often resorts the definitions of data mining problems found in the to implementing new algorithms and variations from literature; should support user-defined constraints and scratch.

Timed Failure Propagation Graphs (TFPGs) are a formalism used in industry to describe failure propagation in a dynamic partially observable system. TFPGs are commonly used to perform model-based diagnosis. As in any model-based diagnosis approach, however, the quality of the diagnosis strongly depends on the quality of the model. Approaches to certify the quality of the TFPG are limited and mainly rely on testing. In this work we address this problem by leveraging efficient Satisfiability Modulo Theories (SMT) engines to perform exhaustive reasoning on TFPGs. We apply model-checking techniques to certify that a given TFPG satisfies (or not) a property of interest. Moreover, we discuss the problem of refinement and diagnosability testing and empirically show that our technique can be used to efficiently solve them.

Lifschitz and Turner introduced the notion of the splitting set and provided a method to divide a logic program into two parts. They showed that the task of computing the answer sets of the program can be converted into the tasks of computing the answer sets of these parts. However, the empty set and the set of all atoms are the only two splitting sets for many programs, then these programs cannot be divided by the splitting method. In this paper, we extend Lifschitz and Turner's splitting set theorem to allow the program to be split by an arbitrary set of atoms, while some new atoms may be introduced in the process. To illustrate the usefulness of the result, we show that for some typical programs the splitting process is efficient and the program simplification problem can be investigated using the concept of splitting.

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.

We analyze the relative expressiveness of the two-valued semantics of abstract argumentation frameworks, normal logic programs and abstract dialectical frameworks. By expressiveness we mean the ability to encode a desired set of two-valued interpretations over a given propositional vocabulary A using only atoms from A. While the computational complexity of the two-valued model existence problem for all these languages is (almost) the same, we show that the languages form a neat hierarchy with respect to their expressiveness. We then demonstrate that this hierarchy collapses once we allow to introduce a linear number of new vocabulary elements.

Modularity is an essential aspect of knowledge representation theory and practice. It has received substantial attention. We introduce model-based modular systems, an abstract framework for modular knowledge representation formalisms, similar in scope to multi-context systems but employing a simpler information-flow mechanism. We establish the precise relationship between the two frameworks, showing that they can simulate each other. We demonstrate that recently introduced modular knowledge representation formalisms integrating logic programming with satisfiability and, more generally, with constraint satisfaction can be cast as modular systems in our sense. These results show that our formalism offers a simple unifying framework for studies of modularity in knowledge representation.

Since Assumption-Based Argumentation (ABA) was introduced in the nineties,the structure and semantics of an ABA framework have been studied exclusively in logical termswithout any graphical representation.Here, we show how an ABA framework and its complete semantics can be displayed in a graph,clarifying the structure of the ABA framework as well as the resulting complete assumption labellings.Furthermore, we show that such an ABA graph can be used to represent the structureand semantics of a logic program (LP), based on the correspondence between the semantics of a LP and an ABA framework encoding this LP.

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.  

Broad application of answer set programming (ASP) for declarative problem solving requires the development of tools supporting the coding process. Program debugging is one of the crucial activities within this process. Modern ASP debugging approaches allow efficient computation of possible explanations of a fault. However, even for a small program a debugger might return a large number of possible explanations and selection of the correct one must be done manually. In this paper we present an interactive query-based ASP debugging method which extends previous approaches and finds the preferred explanation by means of observations. The system automatically generates a sequence of queries to a programmer asking whether a set of ground atoms must be true in all (cautiously) or some (bravely) answer sets of the program. Since some queries can be more informative than the others, we discuss query selection strategies which - given user's preferences for an explanation - can find the most informative query reducing the overall number of queries required for the identification of a preferred explanation.