Reasoning with the maximally consistent subsets (MCS) of the premises is awell-known approach for handling contradictory information. We introduce two argumentation-based methods for doing so: a declarative approach that is related to Dung-style semantics for abstract argumentation, and a computational approach that is based on extensions of Gentzen-type proofs systems. This brings about a new perspective on reasoning with MCS which shows a strong link between the latter and argumentation systems, and which can be extended to related formalisms. A by-product of this is the introduction of a dynamic proof system for classical logic and rebuttal attacks, which is sound and complete with respect to Dung's stable semantics for the associated argumentation framework.

Logical argumentation is a well-known approach to modelling nonmonotonic reasoning with conflicting information. In this paper we provide a proof-theoretic study of properties of logical argumentation frameworks. Given some desiderata in terms of rationality postulates, we consider the conditions that an argumentation framework should fulfill for the desiderata to hold. The rationality behind this approach is to assist designers to plug-in'' pre-defined formalisms according to actual needs. This work extends related research on the subject in several ways: more postulates are characterized, a more abstract notion of arguments is considered, and it is shown how the nature of the attack rules (subset attacks versus direct attacks) affects the properties of the whole setting.

We introduce an abductive method for a coherent integration of independent data-sources. The idea is to compute a list of data-facts that should be inserted to the amalgamated database or retracted from it in order to restore its consistency. This method is implemented by an abductive solver, called Asystem, that applies SLDNFA-resolution on a meta-theory that relates different, possibly contradicting, input databases. We also give a pure model-theoretic analysis of the possible ways to `recover' consistent data from an inconsistent database in terms of those models of the database that exhibit as minimal inconsistent information as reasonably possible. This allows us to characterize the `recovered databases' in terms of the `preferred' (i.e., most consistent) models of the theory. The outcome is an abductive-based application that is sound and complete with respect to a corresponding model-based, preferential semantics, and -- to the best of our knowledge -- is more expressive (thus more general) than any other implementation of coherent integration of databases.

Abstract: We introduce an abductive method for a coherent integration of independent data-sources. The idea is to compute a list of data-facts that should be inserted to the amalgamated database or retracted from it in order to restore its consistency. This method is implemented by an abductive solver, called Asystem, that applies SLDNFA-resolution on a meta-theory that relates different, possibly contradicting, input databases. We also give a pure model-theoretic analysis of the possible ways to `recover' consistent data from an inconsistent database in terms of those models of the database that exhibit as minimal inconsistent information as reasonably possible. This allows us to characterize the `recovered databases' in terms of the `preferred' (i.e., most consistent) models of the theory. The outcome is an abductive-based application that is sound and complete with respect to a corresponding model-based, preferential semantics, and -- to the best of our knowledge -- is more expressive (thus more general) than any other implementation of coherent integration of databases.