We study the problem of reasoning from incoherent answer set programs, i.e., from logic programs that do not have an answer set due to cyclic dependencies of an atom from its default negation. As a starting point we consider so-called semi-stable models which have been developed for this purpose building on a program transformation, called epistemic transformation. We give a model-theoretic characterization of this semantics, considering pairs of two-valued interpretations of the original program, rather than resorting to its epistemic transformation. Moreover, we show some anomalies of semi-stable semantics with respect to basic epistemic properties and propose an alternative semantics satisfying these properties. In addition to a model-theoretic and a transformational characterization of the alternative semantics, we prove precise complexity results for main reasoning tasks under both semantics.

Horn fragments of Description Logics (DLs) have gained popularity because they provide a beneficial trade-off between expressive power and computational complexity and, more specifically, are usually tractable w.r.t. data complexity. Despite their potential, and partly due to the intricate interaction of nominals (O), inverses (I) and counting (Q), such fragments had not been studied so far for the DLs SHOIQ and SROIQ that underly OWL 1 and 2. In this paper, we present a polynomial and modular translation from Horn-SHOIQ knowledge bases into DATALOG, which shows that standard reasoning tasks are feasible in deterministic single exponential time. This improves over the previously known upper bounds, and contrasts the known NEXPTIME completeness of full SHOIQ. Thereby, Horn-SHOIQ stands out as the first EXPTIME complete DL that allows simultaneously for O, I, and Q. In addition, we show that standard reasoning in Horn-SROIQ is 2-EXPTIME complete. Despite their high expressiveness, both Horn-SHOIQ and Horn-SROIQ have polynomial data complexity. This makes them particularly attractive for reasoning in semantically enriched systems with large data sets. A promising first step in this direction could be achieved exploiting existing DATALOG engines, along the lines of our translation.

Description Logics (DLs) are knowledge representation formalisms that provide, for example, the logical underpinning of the W3C OWL standards. Conjunctive queries (CQs), the standard query language in databases, have recently gained significant attention for querying DL knowledge bases. Several different techniques are available for a wide range of DLs. Nevertheless, for OWL 1 DL and OWL 2 DL, decidability of CQ entailment is an open problem. So far, the combination of nominals, inverse roles, and number restrictions caused unsolvable problems. We tackle this problem and present a decidability result for entailment of unions of CQs in a DL with all three problematic constructors. For queries with only simple roles, our result also shows decidability in the logic that underpins OWL 1 DL and we believe that the presented results will pave the way for further progress towards CQ entailment decision procedures for OWL.

We identify three classes of four-state paraconsistent logics according to their different approaches towards the disjunctive syllogism, and investigate three representatives of these approaches: Quasi-classical logic, which always accepts this principle, Belnap's logic, that rejects the disjunctive syllogism altogether, and a logic of inconsistency minimization that restricts its application to consistent fragments only. These logics are defined in a syntactic and a semantic style, which are linked by a simple transformation. It is shown that the three formalisms accommodate knowledge minimization, and that the most liberal formalism towards the disjunctive syllogism is also the strongest among the three, while the most cautious logic is the weakest one.

We present a decidable class of first-order formulas in the general theory of stable models that can be instantiated even in the presence of function constants. The notion of an argument-restricted formula presented here is a natural generalization of both the notion of an argument-restricted program and the notion of a semi-safe sentence that have been studied in different contexts. Based on this new notion, we extend the notion of safety defined by Cabalar, Pearce and Valverde to arbitrary formulas that allow function constants, and apply the result to $\raspl$ programs and programs with arbitrary aggregates, ensuring finite groundability of those programs in the presence of function constants. We also show that under a certain syntactic condition, argument-restricted formulas can be turned into argument-restricted programs.

In this paper, we propose an alternative notion, called weak forgetting, of forgetting a set of predicates in a first-order theory. One important feature of this new notion is that the result of weak forgetting is always first-order expressible. In contrast, this is not the case for the traditional notion of forgetting, called strong forgetting, introduced by Lin and Reiter. As a consequence, these two notions are not exactly the same. Interestingly, we prove that they coincide when the result of strong forgetting is first-order expressible. We also present a representation theorem to characterize weak forgetting from different aspects.

Existing action calculi provide rich, declarative formalisms for reasoning about actions. BDI-based programming languages like AgentSpeak, on the other hand, are procedural and geared towards practical applications of cognitive agents. In this paper, we close the gap between these two lines of research by integrating action calculi and AgentSpeak programs. Specifically, we develop a new and purely declarative semantics for AgentSpeak, which paves the way for combining this language with any suitable action calculus in a strictly modular fashion. As the main technical result, we prove that the new declarative semantics is correct wrt. the standard operational semantics for AgentSpeak. This provides the basis for a modular integration of a BDI-based agent programming language with sophisticated methods for reasoning about actions.

In this paper we introduce dialectical frameworks, a powerful generalization of Dung-style argumentation frameworks where each node comes with an associated acceptance condition. This allows us to model different types of dependencies, e.g. support and attack, as well as different types of nodes within a single framework. We show that Dung's standard semantics can be generalized to dialectical frameworks, in case of stable and preferred semantics to a slightly restricted class which we call bipolar frameworks. We show how acceptance conditions can be conveniently represented using weights respectively priorities on the links and demonstrate how some of the legal proof standards can be modeled based on this idea.

In this paper, we propose a progression semantics for first-order answer set programs. Based on this new semantics, we are able to define the notion of boundedness for answer set programming. We prove that boundedness coincides with the notions of recursion-free and loop-free under program equivalence, and is also equivalent to first-order definability of answer set programs on arbitrary structures.

Maximality is a desirable property of paraconsistent logics, motivated by the aspiration to tolerate inconsistencies, but at the same time retain from classical logic as much as possible. In this paper, we introduce the strongest possible notion of maximal paraconsistency, and investigate it in the context of logics that are based on deterministic or non-deterministic three-valued matrices. We first show that most of the logics that are based on properly non-deterministic three-valued matrices are not maximally paraconsistent. Then we show that in contrast, in the deterministic case all the natural three-valued paraconsistent logics are maximal. This includes well-known three-valued paraconsistent logics like P1, LP, J3, PAC and SRM3, as well as any extension of them obtained by enriching their languages with extra three-valued connectives.