External Transaction Logic ( ETR ) is an extension of logic programming useful to reason about the behaviour of agents that have to operate in a transactional way, in a two-fold environment: an internal knowledge base defining the agent's internal knowledge and rules of behaviour, and an external world where it executes actions and interacts with other entities. Actions performed by the agent in the external world may fail, e.g. because their preconditions are not met, or because they violate some norm of the external environment. The failure to execute some action should lead, in the internal knowledge base, to its complete rollback, following the standard ACID transaction model used e.g. in databases. Since it is impossible to rollback external actions performed in the outside world, external consistency must be achieved by executing compensating operations (or repairs) that revert the effects of the initial executed actions. In ETR , repairs are stated explicitly in the program. With it, every performed external action is explicitly associated with its corresponding compensation or repair. Such user-defined repairs provide no guarantee to revert the effects of the original action. In this article, we define how ETR can be extended to automatically calculate compensations in case of failure. For this, we start by explaining how the semantics of Action Languages can be used to model the external domain of ETR , and how we can use it to reason about the reversals of actions.

Abstract Ontologies and rules are usually loosely coupled in knowledge representation formalisms. In fact, ontologies use open-world reasoning, while the leading semantics for rules use non-monotonic, closed-world reasoning. One exception is the tightly coupled framework of Minimal Knowledge and Negation as Failure (MKNF), which allows statements about individuals to be jointly derived via entailment from ontology and inferences from rules. Nonetheless, the practical usefulness of MKNF has not always been clear, although recent work has formalized a general resolution-based method for querying MKNF when rules are taken to have the well-founded semantics, and the ontology is modeled by a general oracle. That work leaves open what algorithms should be used to relate the entailments of the ontology and the inferences of rules. In this paper we provide such algorithms, and describe the implementation of a query-driven system, CDF-Rules, for hybrid knowledge bases combining both (non-monotonic) rules under the well-founded semantics and a (monotonic) ontology, represented by the Coherent Description Framework Type-1 ( $\mathcal{ALCQ}$ ) theory.

Hybrid MKNF knowledge bases are one of the most prominent tightly integrated combinations of open-world ontology languages with closed-world (nonmonotonic) rule paradigms. Based on the logic of minimal knowledge and negation as failure (MKNF), the definition of Hybrid MKNF is parametric on the description logic (DL) underlying the ontology language, in the sense that nonmonotonic rules can extend any decidable DL language. Two related semantics have been defined for Hybrid MKNF: one that is based on the Stable Model Semantics for logic programs and one on the Well-Founded Semantics (WFS). Under WFS, the definition of Hybrid MKNF relies on a bottom-up computation that has polynomial data complexity whenever the DL language is tractable. Here we define a general query-driven procedure for Hybrid MKNF that is sound with respect to the stable model-based semantics, and sound and complete with respect to its WFS variant. This procedure is able to answer a slightly restricted form of conjunctive queries, and is based on tabled rule evaluation extended with an external oracle that captures reasoning within the ontology. Such an (abstract) oracle receives as input a query along with knowledge already derived, and replies with a (possibly empty) set of atoms, defined in the rules, whose truth would suffice to prove the initial query. With appropriate assumptions on the complexity of the abstract oracle, the general procedure maintains the data complexity of the WFS for Hybrid MKNF knowledge bases. To illustrate this approach, we provide a concrete oracle for EL + , a fragment of the lightweight DL EL ++ . Such an oracle has practical use, as EL ++ is the language underlying OWL 2 EL, which is part of the W3C recommendations for the Semantic Web, and is tractable for reasoning tasks such as subsumption. We show that query-driven Hybrid MKNF preserves polynomial data complexity when using the EL + oracle and WFS.

A general top-down algorithmization for the Well-Founded MKNF Semantics – a semantics for combining rules and ontologies – was recently defined based on an extension of SLG resolution for Logic Programming with an abstract oracle to the parametric ontology language. Here we provide a concrete oracle with practical usage, namely for ℰℒ+which is tractable for reasoning tasks like subsumption. We show that the defined oracle remains tractable (wrt. data complexity) so that the combined (query-driven) approach of non-monotonic rules with that oracle is tractable as well.

With the advent of the Semantic Web, the question becomes important how to best combine open-world based ontology languages, like OWL, with closed-world rules paradigms. One of the most mature proposals for this combination is known as Hybrid MKNF knowledge bases [11], which is based on an adaptation of the stable model semantics to knowledge bases consisting of ontology axioms and rules. In this paper, we propose a well-founded semantics for such knowledge bases which promises to provide better efficiency of reasoning, which is compatible both with the OWL-based semantics and the traditional well-founded semantics for logic programs, and which surpasses previous proposals for such a well-founded semantics by avoiding some issues related to inconsistency handling.

Abductive logic programming offers a formalism to declaratively express and solve problems in areas such as diagnosis, planning, belief revision and hypothetical reasoning. Tabled logic programming offers a computational mechanism that provides a level of declarativity superior to that of Prolog, and which has supported successful applications in fields such as parsing, program analysis, and model checking. In this paper we show how to use tabled logic programming to evaluate queries to abductive frameworks with integrity constraints when these frameworks contain both default and explicit negation. The result is the ability to compute abduction over well-founded semantics with explicit negation and answer sets. Our approach consists of a transformation and an evaluation method. The transformation adjoins to each objective literal $O$ in a program, an objective literal $\hbox{\it not}(O)$ along with rules that ensure that $\hbox{\it not}(O)$ will be true if and only if $O$ is false. We call the resulting program a dual program. The evaluation method, ABDUAL, then operates on the dual program. ABDUAL is sound and complete for evaluating queries to abductive frameworks whose entailment method is based on either the well-founded semantics with explicit negation, or on answer sets. Further, ABDUAL is asymptotically as efficient as any known method for either class of problems. In addition, when abduction is not desired, ABDUAL operating on a dual program provides a novel tabling method for evaluating queries to ground extended programs whose complexity and termination properties are similar to those of the best tabling methods for the well-founded semantics. A publicly available meta-interpreter has been developed for ABDUAL using the XSB system.

In order to be able to explicitly reason about beliefs, we've introduced a non-monotonic formalism, called the Autoepistemic Logic of Beliefs, AEB, obtained by augmenting classical propositional logic with a belief operator, β. For this language we'v