Proving Theorems in a Multi-Source Environment

1 Introduction

More and more, computer science applications need to use information which is not provided by a single source of information but by several.

This is the case, for instance, when one wants to use several expert systems, each of them dealing with a par­ ticular part of the global problem to be solved. In this case, the knowledge coming from each expert system must be combined. This combination is not necessar­ ily physical and the knowledge may remain distributed among the different systems. However, the set of knowl­ edge necessary to solve the global problem is obtained by virtually grouping the knowledge of the different sys­ tems. It is also the case of distributed databases. Each database stores information concerning a particular ap­ plication domain. When considering a larger domain, one has to federate different databases. Here again, the grouping is virtual since, very often, the different databases are locally managed by other people. Another case of collection of information provided by differen­ t sources can be found in the grouping of beliefs. The classic example is that of a police inspector [C Baral and Subrahmanian, 1992] who questions different witnesses. Each witness has his own beliefs concerning the crime and the inspector has to collect all of them in order to find the clue.

·This work has been financed by the CNRS and the French Ministry of Research

Several problems arise when merging different infor­ mation sources [Cholvy, 1992a]. First of all, there are problems of language : the sources do not necessarily share a common language for describing information. In databases for instance, this happens when the different databases to be merged do not have the same schema. In such a case, translations are necessary [Elmagarmid and Pu, ]. There also are problems of redundancy : a source may provide information which subsumes other information provided elsewhere. In this case, pruning is necessary. Finally, there are problems of consistency. Even if each source is consistent, the global set of in­ formation may be contradictory. This is augmented by the delocalised management of the different information sources. People who need to gather information are not those who manage the different bases and, due to the distribution, the different sources are managed by dif­ ferent people. So the notion of global consistency does not exist, since the sources are independently develope­ d. However, when grouping all of them, the problem of consistency arises.

Our work concerns the last problem : we are interested in defining a logical framework which allows us to rea­ son with information provided by different sources and which does not collapse in case of inconsistency. Classi­ cal logic cannot be used directly in this case since every­ thing is deducible from a contradiction (one can say it collapses in case of inconsistency) . In the next section, we will present different studies which dealt with this problem. We will also present our approach. In section 3, we will present the logic we have defined in order to reason in a multi-source environment . In section 4, we define a theorem prover which implements our approach . It is described as a meta-program and we run it under a PROLOG-like language. Correctness of the theorem prover is proved.

2 Some related work and our proposals

Work dealing with the problem of reasoning in the pres­ ence of inconsistency can be divided into two groups.

• In the first group, we find studies which use classical logics but which eliminate inconsistency in order not to collapse. The main way to discard inconsistency is to manage maximal consistent subsets. Work by [C Baral and Subrahmanian, 1992] belongs to this group. They define several types of theory combina­ tions, mainly based on the maximal consistent sub­ sets of the global theory. Our past work [Cholvy, 1990], [Bauval and Cholvy, 1991], also belongs to this group. In the related domain of database up­ dates, work by [Fagin et al., 1983] and [Kupper et al. , 1984] also privilege maximal consistent subsets, as do [Gardenfors, 1988], [Nebel, 1989] in belief re­ vision area, and [Ginsberg and Smith, 1988] in the problem of reasoning about actions.
• In the second group, we find studies which do not use classical logics. For instance, paraconsistent log­ ics are defined in such a way that some classical theorems (which allow us to derive everything from a contradiction) are not deducible in these logics [Besnard, 1990]. For example, A /1. ..., A -+ B is not a theorem in paraconsistent logics. So a con­ tradiction, say A /1. ..., A, cannot be used to derive anything, say B. Another example of non-classical logic which can manage with inconsistency is the modal logic for reasonine; about updates defined in [Cerro and Herzig, 1986j and [Farinas and Herzig, 1992]. Even if the update is contradictory with the current database , the logic does not collapse.

Besides this classification, another classification could be made : indeed, in each previous group, most of re­ searchers have studied two cases. In a first step, they consider that all the data are equal with regard to the problem of inconsistency. In a second step, they s­ tudied the case where data are associated with extra­ information (tags, labels, degrees of priority, actions to be performed .. . ) which are used to restore consistency. For instance, [Fagin et al., 1983], [C Baral and Subrah­ manian, 1992], [Besnard, 1990], [D. Dubois and Prades, 1992], [Gabbay and Hunter , 1991] present different types of extra-information.

Finally, the previous works could be grouped accord­ ing to another classification : most of them adopt a con­ structive approach in the sense that avoiding inconsisten­ cy leads to construct a new consistent base. Only work by [Cerro and Herzig, 1986] and [Farinas and Herzig, 1992] adopts a hypothetical approach : the logic they define, called assume, allows us to reason with hypo­ thetical updates. The user can then deduce theorems of the form : such a formula will be true if I assume such other formula. The state after the update is never constructed.

As for us, we have defined two logics for reasoning in a multi-source environment which do not collapse under inconsistency, [Cholvy, 1992a] [Cholvy, 1992b] . Both of them allow the user to assume that the different sources of information are totally ordered according to their re­ liability. Our approach is then a hypothetical one. The two logics differ on the attitude they modelize :

• The first logic, called FUSION-S, modelizes a sus­ picious attitude : it consists in suspecting all the information provided by a source if this source con­ tradicts a more reliable source.
• The second logic, called FUSION-T , modelizes a trusting attitude : if an information source contra­ dicts a more reliable source, only the smallest set of contradictory information is suspected.

Let us take the example of a police inspector who ques­ tions witnesses. Assume that a first witness, Bill, said that he saw a black car, while a second, John, said that he saw two men in a white car. An order may reflect the fact that the inspector himself has some conviction (which cannot be denied) or possesses some information which is true : for instance, he went to the meteorologi­ cal station and he is sure that the crime was committed on a foggy day. So, he can assume that John is less re­ liable than Bill, since John was standing too far away from the scene of the crime and, because of the fog , he could not see well. So, the inspector may trust him less. In this case, the inspector will consider that : inspector >Bill >John.

If the inspector adopts the suspiscious attitude, he will conclude only that the car was black, i.e., he suspects all the information provided by John because John contra­ dicts a more reliable witness. If he adopts the trusting attitude, he will conclude that they were two men in a black car. In fact, concerning the colour of the car, he trusts Bill more than John, so he can assume that the colour is black. Concerning the number of persons, John provides new information that does not contradict Bill's account.

In the rest of this paper, we focus on the trusting at­ titude. The next section describes the logic which mod­ elizes it.

Remark 1. As said previously, the trusting attitude suspects the smallest set of information which contra­ dicts more reliable information. In this paper, smallest contradictory sets are pairs of literals : l and ..., l.

We can imagine a more "application-adapted" ap­ proach in which the notion of topics of information [Cazalens, 1992) [Cazalens and Demolombe, 1992), is taken into account in order to characterize the minimal­ ity. For example, assume a meeting in which a person listens to two people. The first is a teacher of logic, the second is a student. The conversation is technical. Im­ plicitely, the person who listens trusts the teacher more than the student. Assume that during the conversation, the student affirms that "the first order logic is decid­ able". Immediately, the teacher denies it and reminds the student of the main result of undecidability of the first order logic. For the person, it is clear that the stu­ dent is not reliable concerning the first order logic. If, later on, the student makes another affirmation about the first order logic, it is quite sure that the listener will not trust him. Indeed, because of the contradiction about the decidability, he rejects any affirmation of the student which "is about" the first order logic. In this case, works previously cited which try to formalize the notion of "is-about", could be used in order to reject a smallest set of information, defined by the domain of the first order logic. An attempt to use the notion of topics of information for a syntactical characterization of updates can be found in [Cholvy, 1993].

Remark 2. In this paper, we assume the existence of a unique order on the different sources of information. Again, we can imagine a more "application-adapted" ap­ proach in which the sources are ordered according to several orders which are topic-dependent .

Let us take the previous example and consider that the teacher of logic (who is an old-fashioned man) and the student are now speaking about pop music. It is quite sure that, regarding "pop music", he will trust the student more than the teacher, i.e., the student will be considered as more reliable than the teacher. So there will be two orders, one for the "logics" topic and one for the "pop music" topic.

An attempt at a formalization of this idea can be found in [Cholvy, 1993].

3 A logic for reasoning in a multi-source environment

In this section, we present a logic which implements the trusting attitude previously introduced.

3.1 The language

We assume that our language L is a finite set of propo­ sitional variables : Pt, P2, ... PL· We note 1, 2 .. n the n information sources we reason with. We will also say the databases to be merged. We assume that the sources (or databases) are finite, satisfiable but not necessarily complete, sets of literals of L.

The logic we define, called FUSION-Tn .. n), is ob­ tained from the propositional logic, augmented with pseudo-modalities i.e., marks on formulas. These pseudo-modalities are :

[iti2··im] F will mean that, when considering the total order on {it . .im}: it> i2,i2 > i3, .. im-t > im, F is true in the database obtained by virtually merging database it and .. database im .

Notice that the general form of these pseudo­ modalities allows us to represent the particular case : [i] F, i=l..n, which means that F is true in database i.

3.2 Semantics

The semantics of FUSION-T(l .. n) is the following : a model ofFUSION-T(l..n) is a pair : I= (W, r), where:

• W is the finite set of all the interpretations of the underlying propositional language L
• r is a finite set of equivalence relations between in­ terpretations in W.

Each pseudo-modality is associated with a relation. So, if [0] is a pseudo-modality, we note R(O) the associ­ ated equivalence relation and R(O) its equivalence class. The equivalence classes are recursively defined by :

Definition. (Satisfaction of formulas) . Let F be a formula of L. Let Fl and F2 be formulas of L'. Let 0 be a total order on a subset of {l..n} . Let M = (W,r) be an interpretation of FUSION-T(l..n)

and let wE W.

Definition. (Valid formulas m FUSION-T(l..n)) . Let F be a formula of L'. F is a valid formula (in FUSION-T(l..n)) <=> V M = (W,r) an interpretation of FUSION-T(l..n), V wE W, FUSION-T(l..n),r,w F F

We note FUSION-T(l .. n) F F, the valid formulas .

3.3 Axiomatics

Let us write 0 an order it··im, m ~ 1. (i.e., it > i2, .. , im-t > im)· By convention, 0 U {im+d is the order it . .imim+l ·

Axioms of FUSION-T(l..n) are:

• (AO) Axioms of the propositional logic
• (Al) [0]..., F-..., [0] F
• (A2) [0] F A [O](F - G) - [0] G
• (A3) [0 U {i}]l +---+ [0]1 V ([i]IA..., [0]..., I) if I is a literal

Inferences rules of FUSION-T(l..n) are :

• (Nee) 1- F ~ 1- [0] F (if F is a propositional formula)
• (MP) 1- F and 1- (F -> G) ~ 1- G

Axiom (A3) expresses the trusting attitude. Indeed, we could decompose it in three axioms :

• (A3.1) (0]1- (0 U {i}J I
• (A3.2) [i]IA..., [0]..., I- [0 U {i}]l

This means that :

• if a literal is true under order 0, then it is still true under order 0 U {i}, for any i, since, by convention, 0 U {i} means that i is the least reliable source.
• if it is the case that a literal is true in database i, and if it is not the case that its negation is true under order 0, then it is the case that it is true under 0 U {i}.
• if it is not the case that a literal is true under order 0 and if it is not the case that it is true in database i then it is not the case that it is true under order 0 U {i}

Remark. This logic will be used to modelize the merging of n databases dbl ... dbn, in the case where they are finite consistent sets of L literals and according to the trusting attitude.

(where lis a literal of Land c a clause of L) .

We will be interested in finding valid formulas of the form : (t/; --> [0] F), i.e., finding formulas F which are true in the database obtained by merging db1 ... dbn, when the order is 0.

We have proved the following facts :

Proposition 1. Let t/J be the formula previously de­ fined. Let F be a formula of L. Let 0 be a total order on a subset of {l..n} . Then :

Proposition 2. With the same assumptions as in proposition 3 :

FUSION-T(l .. n) 1- (t/;- [OJ F) or FUSION-T(l .. n) 1- (t/;-..., [OJ F)

3.4 A quick comparison with the belief revision problem

Let us first recall some definitions [Katsuno and Mendel­ zon, 1991J :

Definition. Let m and m1 be two interpretations. We define the distance between m and m1 by :

d(m,ml) = {p E L : (p E m and p ¢ m1) or (p ¢ m and p E ml) }

Definition. Let m be an interpretation. We define a partial order on a set of interpretations ~m by : m1 ~m m2 {:::=} d(m,ml) ~ d(m,m2)

Then we can prove· that the functions fii defined in section 3.2 are such that : fii (E) = UmER(ii) Min(E, ~m)

So, according to [Katsuno and Mendelzon, 1991], fj(E) is the set of models of belief base DBj updated by E. In other terms, the result of merging two databases ac­ cording to the trusting attitude and such that i >j, is equivalent to updating database j with database i.

Generalisation. Merging n databases 1,2 .. n, ac­ cording to the trusting attitude and given an order : i1 > i2, .. , in-1 > in comes down to updating DBin with the result of the update of DBin-1 with the result of the update .... of DBi2 with DBi1.

4 A theorem prover for this logic

In this section, we deal with the implementation aspects. Our aim is to define a theorem prover for this logic which allows us to answer questions of the form : is formula F true in the merged information sources if the order is 0 ? i.e., to prove theorem [O]F. We suggest using a PROLOG-like language form implementing such a the­ orem prover, in order to reuse its facilities (unification, negation as failure, strategy ... )

In subsection 4.1, we describe a first meta-program which describes a prover for proving formula [OJ!, if I is a literal. This meta-program is a set of definite Horn­ clauses (where negation is explicitely managed with posi­ tive literals) and which can easily be run on a PROLOG­ like interpreter. In subsection 4.2, we give an optimisa­ tion where the negation-as-failure of PROLOG is used to manage the negation . Finally, in section 4.3, we ex­ tend this prover in order to prove formula [OJ F, where F is any propositional formula (written under the con­ junctive normal form) .

4.1 The theorem prover as a meta-program: first v-ersion

Let us consider a meta-language ML, based on language L, defined by :

• constants of ML are literals of L, plus a constant noted nil
• a function noted U . By convention, {i1 . .im} repre­ sents the term: i1 U (i2··· U (im U nil) ... ).
• predicat symbols of ML are : LFUSION, nonLFU­ SION, NIL and nonNIL.

The intuitive semantics of the predicates is the follow­ ing :

• LFUSION(O,l) means that it is the case that literal I is true in the merged databases if the order is 0 .
• nonLFUSION(O,l) means that it is not the case that literal I is true in the merged database if the order is 0
• NIL(O) is true only for nil
• nonNIL(O) is true except if 0 is nil.

4.1.1 The meta-program

Let us consider METAl, the following set of the ML formulas:

1. LFUSION( {i}, 1), for any literal! in database i
2. LFUSION(O,l) 1\ nonNIL(O) --. LFUSION(O U {i}, I)
3. LFUSION( {i},l) 1\ nonLFUSION(O,..., l) 1\ nonNIL(O)--+ LFUSION(O U {i}, I)
4. nonLFUSION({i}, I), for any literal! not in database i
5. LFUSION(O,l) --> nonLFUSION(O, ..., I)
6. nonLFUSION(O,l) 1\ nonLFUSION( {i},l) 1\ nonNIL(O) --. nonLFUSION(O U {i},l)
7. nonNIL(O) , for any 0 except nil

Proposition 3. (soundness and completeness)

Let l be a literal of L, let 0 be a total order on a subset of {l..n} .

METAl 1- LFUSION(O,l) {:::::}

FUSION-T(l..n) 1- (1/J-+ [O]l)

and

METAl 1- nonLFUSION(O,l) {:::::}

FUSION-T(l .. n) 1- (1/J-+-. [0) l)

(To prove the soundness, we consider the fixed point operator FP, associated to METAl which is such that METAl 1- LFUSION(O,l) ===> 3 k LFUSION(O,l) E FPk(0) (resp nonFUSION(O,l)) . We then prove the two points by induction on k. We prove the completeness, jointly for the two points, by induction on the length of the prefixes).

Proposition 4. (Corollary)

Let l be a literal of L and 0 a total order on a subset of {l..n} . Then,

METAl 1- LFUSION(O,l) or

METAl 1- nonLFUSION(O,l)

4.1.2 Implementation

In this first version, PROLOG is used in this meta­ program METAl. The following proposition ensures that, although this meta-program is recursive , PROLOG does not loop when running it .

Proposition 5.

Let l be a literal of L, let 0 be a total order on a sub­ set of {l..n} . The tree developped by PROLOG in or­ der to prove the goal : LFUSION(O,l) (resp nonLFU­ SION(O,l)) in METAl is finite .

(We prove it by induction on the length of the prefix 0)

4.2 Optimisation

The main remark about the previous meta-program con­ cerns the explicit management of the predicate nonFU­ SION. An optimisation can be realised by managing the predicates nonFUSION and nonNIL with negation-as­ failure of PROLOG. This leads to the meta-program, META2:

1. LFUSION( {i}, l) for any literall in database i
2. LFUSION(O,l) 1\-. NIL(O) -+ LFUSION(O U {i}, l)
3. LFUSION( {i} ,l) 1\-. LFUSION(O,-. l) 1\ -. NIL(O) -+ LFUSION(O U {i}, l)
4. NIL(nil)

Proposition 6. Let l be a literal, let 0 be a total order on a subset of { l..n}.

PROLOG fails to prove LFUSION(O,l) in META2 us­ ing the negation-as-failure iff PROLOG proves nonLFU­ SION(O,l) in METAl (without using negation as fail­ ure).

(The proof is immediate)

Proposition 6 and proposition 3 allow us to give:

Proposition 7. Let l be a literal, let 0 be a total order on a subset of {l..n} .

Using negation-as-failure on the meta-progran META2, PROLOG succeeds in proving LFUSION(O,l) iff

FUSION-T(l..n) 1- ( 1/J -+ [O)l) ; it fails iff

FUSION-T(l..n) 1- (1/J-+-. [0) l)

4.3 Extension to any propositional formula

We consider the following meta-program, META3, ob­ tained from META2 by adding three axioms for the man­ agement of conjunctions and disjunctions :

1. LFUSION( {i}, l) for any literall in database i
2. LFUSION(O,l) 1\-. NIL(O)-+ LFUSION(O U {i}, l)
3. LFUSION( {i},l) 1\-. LFUSION(O,-. l) 1\-. NIL(O) -+ LFUSION(O U {i}, l)
4. NIL(nil)
5. CFUSION(O,nil)
6. DFUSION(O,d) 1\ CFUSION(O,c) -+ CFUSION(O,d U c)
7. LFUSION(O,l) -+ DFUSION(O,l U d)
8. DFUSION(O,d) -+ DFUSION(O, l U d)

Proposition 8.

Let F be a formula under its conjunctive normal form. Let 0 be a total order on a subset of { l..m} . Using negation-as-failure on the meta-progran META3 , PROLOG proves the goal CFUSION(O,F) iff FUSION-T(l..n) 1- (1/J-+ [O)F) ; it fails iff FUSION-T(l..) 1- (1/J-+-. [0) F)

(We prove the if condition by using the fixed point operator FP and show that : if PROLOG proves DFU­ SION(O,D), then FUSION-T(l..n) 1- (1/J -+ [O)D), and if PROLOG proves CFUSION(O,C), then

FUSION-T(l..n) 1- (1/J-+ [O]C).

We prove the only-if condition by decomposing F in a conjunction of disjunctions of literals. Proposition 2 is then used for the failing case)

5 Conclusion

In this paper, we have dealt with the problem of rea­ soning in a multi-source environment by focusing on the global consistency of information. We have shown that this problem is a particular case of reasoning with incon­ sistency. For discarding inconsistency, we have suggested considering the relative reliability of the different infor­ mation sources. This comes down to considering a total order on the sources. There are different ways to use this order to avoid the inconsistency but in this paper we have focused on one attitude, called trusting : when two sources are contradictory, it consists in rejecting the minimal contradictory information which is provided by the less reliable source.

Our aim was to define a logic that would allow the user to reason in a multi-source environment according to a hypothetical approach : the merging of the differ­ ent sources is never done, i.e., the database obtained by merging the information coming from the differen­ t sources is never construted. The user only assumes the order of the sources and tries to derive true formula in this assumed database. As far as we know, only the work cited in section 2 for database updates adopts such a hypothetical approach.

The semantics we have attached to this attitude is in terms of possible models and is an extension of the semantics defined for belief base updates. The notion of "nearest" models is defined in terms of complementary literals. The semantics is appropriate even if information is extended to clauses [Cholvy, 1993]. Unfortunately, the axiomatics we have given, and the theorem prover we have defined, are only adequate for literal information.

In addition, one can wonder what happens if the order on the sources is not total. In this case, we find again the problem of reasoning with inconsistency with no extra­ information to restore consistency. Solutions briefly de­ scribed in section 2 could be adapted here leading to a formalism which mixes our logics and a mechanism to avoid inconsistency (management of maximal consistent subsets for instance). But this needs to be studied more carefully.

Finally, in section 2, we have shown that another se­ mantics could be attached to the reasoning in a multi­ source environment. It consists in taking into accoun­ t notions like topics of information. This application­ oriented notion could be used to give a new definition of minimality as well as an extension to several orders on sources of information.