Multi-context systems (MCS) are a powerful framework for interlinking heterogeneous knowledge sources. They model the flow of information among different reasoning components (called contexts) in a declarative way, using so-called bridge rules, where contexts and bridge rules may be nonmonotonic. We considerably generalize MCS to managed MCS (mMCS): while the original bridge rules can only add information to contexts, our generalization allows arbitrary operations on context knowledge bases to be freely defined, e.g., deletion or revision operators. The paper motivates and introduces the generalized framework and presents several interesting instances. Furthermore, we consider inconsistency management in mMCS and complexity issues.

We analyze the complexity of reasoning in EL with defeasible inclusions, and extend previous results by tightening lower and upper complexity bounds and by relaxing some syntactic restrictions. We further extend the old framework by supporting arbitrary priority relations over defeasible inclusions.

We present a unifying approach to the efficient evaluation of propositional answer-set programs. Our approach is based on backdoors which are small sets of atoms that represent "clever reasoning shortcuts" through the search space. The concept of backdoors is widely used in the areas of propositional satisfiability and constraint satisfaction. We show how this concept can be adapted to the nonmonotonic setting and how it allows to augment various known tractable subproblems, such as the evaluation of Horn and acyclic programs. In order to use backdoors we need to find them first. We utilize recent advances in fixed-parameter algorithmics to detect small backdoors. This implies fixed-parameter tractability of the evaluation of propositional answer-set programs, parameterized by the size of backdoors. Hence backdoor size provides a structural parameter similar to the treewidth parameter previously considered. We show that backdoor size and treewidth are incomparable, hence there are instances that are hard for one and easy for the other parameter. We complement our theoretical results with first empirical results.

This paper studies a computational logic for dishonest reasoning. We introduce logic programs with disinformation to represent and reason with dishonesty. We then consider two different cases of dishonesty: deductive dishonesty and abductive dishonesty. The former misleads another agent to deduce wrong conclusions, while the latter interrupts another agent to abduce correct explanations. In deductive or abductive dishonesty, an agent can perform different types of dishonest reasoning such as lying, bullshitting, and withholding information. We show that these different types of dishonest reasoning are characterized by extended abduction, and address their computational methods using abductive logic programming.

Consequence-based ontology reasoning procedures have so far been known only for Horn ontology languages. A difficulty in extending such procedures is that non-Horn axioms seem to require reasoning by case, which causes non-determinism in tableau-based procedures. In this paper we present a consequence-based procedure for ALCH that overcomes this difficulty by using rules similar to ordered resolution to deal with disjunctive axioms in a deterministic way; it retains all the favourable attributes of existing consequence-based procedures, such as goal-directed “one pass” classification, optimal worst-case complexity, and “pay-asyou- go” behaviour. Our preliminary empirical evaluation suggests that the procedure scales well to non-Horn ontologies.

Model checking is one of the most effective techniques in automated system verification. Although this technique can handle complex verifications, model checking tools usually do not give any suggestions on how to repair inconsistent system models. In this paper, we show that approaches developed to update models of Computation Tree Logic (CTL) cannot deal with all kinds of changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context.

Fages [1994] introduces the notion of well-supportedness as a key requirement for the semantics of normal logic programs and characterizes the standard answer set semantics in terms of the well-supportedness condition. With the property of well-supportedness, answer sets are guaranteed to be free of circular justifications. In this paper, we extend Fages’ work to description logic programs (or DL-programs). We introduce two forms of well-supportedness for DL-programs. The first one defines weakly well-supported models that are free of circular justifications caused by positive literals in rule bodies. The second one defines strongly well-supported models that are free of circular justifications caused by either positive or negative literals. We then define two new answer set semantics for DL-programs and characterize them in terms of the weakly and strongly well-supported models, respectively. The first semantics is based on an extended Gelfond-Lifschitz transformation and defines weakly well-supported answer sets that are free of circular justifications for the class of DL-programs without negative dl-atoms. The second semantics defines strongly well-supported answer sets which are free of circular justifications for all DL-programs. We show that the existing answer set semantics for DL-programs, such as the weak answer set semantics, the strong answer set semantics, and the FLP-based answer set semantics, satisfy neither the weak nor the strong well-supportedness condition, even for DL-programs without negative dl-atoms. This explains why their answer sets incur circular justifications.

In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation.

In a seminal paper, Lin and Reiter introduced the notion of progression of basic action theories. Unfortunately, progression is second-order in general. Recently, Liu and Lakemeyer improve on earlier results and show that for the local-effect and normal actions case, progression is computable but may lead to an exponential blow-up. Nevertheless, they show that for certain kinds of expressive first-order knowledge bases with disjunctive information, called proper+, it is efficient. However, answering queries about the resulting state is still undecidable. In this paper, we continue this line of research and extend proper+ to include functions. We prove that their progression wrt local-effect, normal actions, and range-restricted theories, is first-order definable and efficiently computable. We then provide a new logically sound and complete decision procedure for certain kinds of queries.

The ASPIC+ framework is intermediate in abstraction between Dung's argumentation framework and concrete instantiating logics. This paper generalises ASPIC+ to accommodate classical logic instantiations, and adopts a new proposal for evaluating extensions: attacks are used to define the notion of conflict-free sets, while the defeats obtained by applying preferences to attacks, are exclusively used to determine the acceptability of arguments. Key properties and rationality postulates are then shown to hold for the new framework.