We develop a novel absorption technique for large collections of factual assertions about individual objects. These assertions are commonly accompanied by implicit background knowledge and form a knowledge base. Both the assertions and the background knowledge are expressed in a suitable language of Description Logic and queries over such knowledge bases can be expressed as assertion retrieval queries. The proposed absorption technique significantly improves the performance of such queries, in particular in cases where a large number of object features are known for the objects represented in such a knowledge base. In addition to the absorption technique we present the results of a preliminary experimental evaluation that validates the efficacy of the proposed optimization.

In this paper, we propose a semantic forgetting for arbitrary logic programs(or propositional theories) under answer set semantics,called HT-forgetting. The HT-forgetting preserves strong equivalence in the sense that strongly equivalent logic programs will remain strongly equivalent after forgetting the same set of atoms. The result of an HT-forgetting is always expressible by a logic program, and in particular, the result of an HT-forgetting in a Horn program is expressible in a Horn program; and a representation theorem shows that HT-forgetting can be precisely characterized by Zhang-Zhou's four forgetting postulates under the logic of here-and-there. We also reveal underlying connections between HT-forgetting and classical forgetting, and provide complexity results for decision problems.

We are witnessing an explosion of available data from the Web, government authorities, scientific databases, sensors and more. Such datasets could benefit from the introduction of rule sets encoding commonly accepted rules or facts, application- or domain-specific rules, commonsense knowledge etc. This raises the question of whether, how, and to what extent knowledge representation methods are capable of handling the vast amounts of data for these applications. In this paper, we consider nonmonotonic reasoning, which has traditionally focused on rich knowledge structures. In particular, we consider defeasible logic, and analyze how parallelization, using the MapReduce framework, can be used to reason with defeasible rules over huge data sets. Our experimental results demonstrate that defeasible reasoning with billions of data is performant, and has the potential to scale to trillions of facts.

Belief revision studies strategies about how agents revise their belief states when receiving new evidence.  Both in classical belief revision and in epistemic revision, a new input is either in the form of a (weighted) propositional formula or a total pre-order (where the total pre-order is considered as a whole).  However, in some real-world applications, a new input can be a partial pre-order where each unit that constitutes the partial pre-order is important and should be considered individually. To address this issue,  in this paper, we study how a partial pre-order representing the prior epistemic state can be revised by another partial pre-order (the new input) from a different perspective, where the revision is conducted recursively on the individual units of partial pre-orders.  We propose different revision operators (rules), dubbed the extension, match, inner and outer revision operators, from different revision points of view. We also analyze several properties for these operators.

Within the recently proposed Universal Booleanization framework, we consider the Cumulative constraint, for which the original Boolean encoding proves ineffective, and present a new Boolean encoding that causes the SAT solver to simulate, largely, the search strategy used by some of the best-performing native methods. Apart from providing motivation for future research in a similar direction, we obtain a significantly enhanced version of Universal Booleanization for problems containing Cumulative constraints.

This paper presents a characterisation of and definitions for the phenomenon of masking in the context of justifications for entailments in ontologies. In essence masking is present within a justification, over a set of justifications, or over a complete ontology when the number of justifications for an entailment does not reflect the number of reasons for that entailment. Four types of masking are defined in this paper: Internal Masking, Cross Masking, External Masking and Shared Core Masking. The results of an empirical study are presented which shows that the phenomenon of masking is prevalent throughout ontologies with non-trivial entailments in the NCBO BioPortal corpus. Out of 72 ontologies, 53 exhibited some form of masking, with 9 ontologies exhibiting internal masking, 23 ontologies exhibiting external masking, and 53 ontologies exhibiting shared core masking.

Temporal logics can be used in reasoning about actions for specifying constraints on domain descriptions and temporal properties to be verified. In this paper, we exploit Bounded Model Checking (BMC) techniques in the verification of Dynamic Linear Time Temporal Logic (DLTL) properties of an action theory, which is formulated in a temporal extension of Answer Set Programming (ASP). To achieve completeness, we propose an approach to BMC which exploits the Buechi automaton construction while searching for a counterexample. We provide an encoding in ASP of the temporal action domain and of Bounded Model Checking of DLTL formulas.

The advance of Internet and Sensor technology has brought about new challenges evoked by the emergence of continuous data streams. While existing data-stream management systems allow for high-throughput stream processing, they lack complex reasoning capacities. We address this shortcoming and elaborate upon an approach to knowledge-intense stream reasoning based on Answer Set Programming (ASP). The emphasis thus shifts from rapid data processing to complex reasoning. To accommodate this in ASP, we develop new techniques that allow us to formulate problem encodings dealing with emerging as well as expiring data in a seamless way. We thus propose novel language constructs and modeling techniques for specifying and reasoning with time-decaying logic programs.

Belief merging aims at extracting a coherent and informative view from a set of belief bases. A first requirement for belief merging operators is to obey basic rationality conditions. Another expected property is to preserve as much information as possible from the input bases. In this paper, we show how new merging operators, called compositional operators, can be defined from existing ones. Such operators aim at offering a higher discriminative power than the merging operators on which they are based, without leading to a complexity shift or losing rationality postulates. We identify some sufficient conditions for ensuring that rationality is fully preserved by composition.

We describe the application of assumption-based argumentation (ABA) to a domain of medical knowledge derived from clinical trials of drugs for breast cancer. We adapt an algorithm for calculating the admissible semantics for ABA frameworks to take account of preferences and describe a prototype implementation which uses variant-based parallel computation to improve the efficiency of query answering.