The general context of this work is the problem of merging data provided by several sources which can be contradictory. Focusing on the case when the information sources do not contain any disjunction, this paper first defines a propositional modal logic for reasoning with data obtained by merging several information sources according to a majority approach. Then it defines a theorem prover to automatically deduce these merged data. Finally, it shows how to use this prover to implement a query evaluator which answers queries adressed to several databases. This evaluator is such that the answer to a query is the one that could be computed by a classical evaluator if the query was adressed to the merged databases. The databases we consider are made of an extensional part, i.e. a set of positive or negative ground literals, and an intensional part i.e. a set of first order function-free clauses. A restriction is imposed to these databases in order to avoid disjunctive data.
展开▼