Analogy and Abduction in Automated Deduction

1 Introduction

Analogy is in the very heart of human reasoning, in particular in Mathematics. Roughly speaking, reason­ ing by analogy consists in using informations deduced from the solving of a given problem or set of problems (the source problems) for solving a new one (the tar­ get problem). In Artificial Intelligence and Automated Deduction, the mechanization of this approach is a cru­ cial issue (see for example [Bledsoe, 1977; Plaisted, 1981 ; Hall, 1989]) . Moreover analogy is also an intrinsically interesting way of reasoning: discovering similitaries be­ tween existing proofs or theorems can be of highest importance (for instance in mathematical practice and teaching). As far as we know, in all the existing works in theorem-proving, analogy is used for finding the proof of a given target theorem from an existing one. This view of analogy is very limited since analogy can obviously be also useful if the target or source problems are not theo­ rems: in this case one can try to find a counter-example of the target conjecture by using counter-examples of the source non-theorems. In this paper we give an uni­ fying treatment of these two cases (theorems and non­ theorems) . No assumption is made about the way these proofs and counter-examples are generated (any existing method for search for proofs or counter-examples can be used: (hyper)resolution or tableaux-based methods, connexion method, but also (finite) model builder such as FINDER [Slaney, 1993], SEM [Zhang and Zhang, 1995] or the method RAMC [Bourely et al. , 1994]looking simultaneously for a proof or a counter-example of a given formula :F.

Other approaches have been proposed to tackle the problem of analogy by second-order means. In [Boy de la Tour and Caferra, 1987], the paradigm of "propositions as types" is used and proofs are represented as terms. Higher-order functions are then applied to transform the base proof into the target one. In [Kolbe and Walther, 1995], higher-order evaluation techniques are used tore­ fine the problem and ultimately have its premisses match with axioms of the calculus, allowing lemma speculation as a side effect. However, both approaches only deal with proofs (not counter-examples). To the best of our knowledge there is no other approaches allowing to deal with model building by analogy in first-order logic.

To make the presentation of the method shorter , we assume that the problems are specified in clausal form and that we use a refutational approach. Therefore, formulae are sets of clauses, proofs are refutations and counter-examples are models.

Analogy and abductive reasoning

According to Peirce [Hartshorne et al., ], analogy can be seen as an induction and an abduction followed by a de­ duction. Our approach to analogy follows directly these steps. It can be summarized as follows. We assume a knowledge base/( containing theorems with their proofs and non-theorems associated with. counter-examples.

Generalization step. The first step consists in a generalization occurring at the presentation of a new source formula :F s to /(. :F s is transformed into a more general formula and stored into the knowledge base. This corresponds to the inductive part of analogy.

Matching step. The second step applies when a new target conjecture :FT is considered. It consists in trying to find one (or more) "analogical" formulae in/( . Then the proof or the counter-example of the conjecture :FT is built from the proofs/counter-examples of the formulae in /(. This corresponds to the deductive part of analogy.

However in most cases :FT cannot be directly (dis) proved by using only the information in /( (this is obviously possible only if FT is an instance of a problem inK) . However, even if a proof or a counter-example of FT cannot be straightforwardly deduced from the known formulae, the use of the informations stored in K, will very likely provide interesting hints for finding a proof or a counter-example of :FT . For example it can guide lemmata generation that could be completed later by us­ ing any existing theorem prover or model builder. This corresponds to the abductive part of analogy: finding hy­ potheses that allows to prove or to disprove the target conjecture.

The generalization step has been precisely defined in [Bourely et al. , 1996], where an algorithm is given to transform any formula :F into a "more general formula" :Fgen. The matching step is defined in [Defourneaux and Peltier, 1997]. In this paper we focus mainly on the ab­ ductive part of analogical reasoning, that is to say on the generation of lemmata. We propose a partial matching algorithm especially devoted to finding such lemmata, i.e. abduction will be incorporated to step 2.

Abductive reasoning is the process of generating the explanations of a given fact (see for example [Polya, 1973; Pople, 1973; Console et al., 1991; Hobbs et al. , 1993]). It has deep connections with other forms of reasoning such as model building [Inoue et al., 1993; Console et al., 1991]. Aristotle calls abduction a syllogism "in which the major is sure and the minor only probable" (see [La­ lande, 1980], page 1). More recently, it is defined by Peirce [Peirce, 1955] as the process of finding the minor premise from a major premise and the conclusion: for example "infer" A from A => B and B. Peirce clearly points out the importance of abductive reasoning in sci­ ence (he gave as a paradigm the discovery of Kepler's laws) . From a deductive point of view, this inference is clearly not sound. However it provides interesting infor­ mations for proving B, since A can be considered as a lemma, whose proof immediately yields a proof of B.

The aim of this paper is to show how to use anal­ ogy for generating such lemmata. Since our approach deals with simultaneous search for proofs and counter­ examples, the notion of lemma is much more general than the standard one: it can be either a conjecture that (if it is true) is sufficient for proving B or a partial counter- example that must be completed and extended for finding a counter-example of B .

2 Basic notions

We assume the reader is familiar with the usual termino logy of First-Order Logic and Automated Deduction. We briefly review most of the basic notions used throughout this work.

Let E be a set of functional symbols, 0 be a set of predicate symbols and X be an (countable) infinite set of variables. Let a be a function mapping each symbol in .:E U 0 to a natural number (the arity ofthe symbol). Function symbols of arity 0 are called constants (denoted by a, b, .. . ). The set of terms r(E, X) is defined as usual over the alphabet :E, V (where V ~ X) . If V is empty, r(E, X) is denoted by r(E) . An atom is of the form P(t 1 , ... , tn) , where P E 0, arity(P) ::;: n and Vi E (l..n].t; E r(E, X) . A literal is either an atom or the negation of an atom. If p is a literal, ..,p denotes the literal with the same predicate symbol and the same arguments than p but with different sign. A clause is a finite set (or disjunction) ofliterals. First-order formulae are built as usual over atoms by using the logical symbols V, /\, -., 3, \( .. .. By Var(E) we denote the set of (free) variables occurring in the expression (term, clause, atom, literal. .. ) E . A term or a clause containing no variables is called ground. The notion of substitution is defined as usual. The result of applying a substitution u to a term t is noted tu. The domain of a substitution u is the set of variables x such that xu¢. x (noted Dom(u)). If for all variables x E Dom(u), xu is ground then u is called ground.

For any set of clauses S we denote by S(S) the set of groJ..tnd instances of clauses in S.

As is well known, a ground clause C' subsumes a ground clause C (noted C' ~. C) iff C' ~ C. If C, C' are two clauses, C ~. C' iff for all D' E S(C'), 3D E S(C)/D ~~ D'.

2.1 Higher order formulae

Step 2 of the method (see Introduction) needs an algo­ rithm transforming a given set of clauses S into a more general one. The latter is represented by second order terms and clauses. Higher-order terms and formulae are built as usual from a signature V, E, 0 by using applica­ tion and abstraction (see [Huet, 1975]) .

The set of types Sk of order k is defined as follows. If k = 1, Sk = {T} (base type). If 'ViE (l..n] .t; E Sk; an~ 8 E sk, and k = 1+max(kt, ... ,k;), then tl X .·. xtn-+ s e sk .

Let S = U: 1 S;. Let (V)u;:s a set of disjoint infinite (countable) sets of variables (called variables of type t). Let V = UteT Vt, let (E)tes a collection of disjoint set of constants of type t . We assume that V n E = 0.

The sets of terms Tt(E, V) of type t are built as usual from V, E using application or abstraction. We denote by r(E, V) = UteT Tt(E, V), the whole set of terms. The definition of formulae, equational formulae, sub­ stitutions, etc. can be extended straightforwardly to higher-order term. We do not give all the definitions (see for example [Lugiez, 1995]) .

Roughly speaking sets of clauses will be represented by sets of generalized clauses i.e. clauses where the function symbols are replaced by variables of order 2.

A generalized formula is a formula such that each bound variable is of order 1, and each free variable of :F is of order 1 or 2 and occurs in a term of the form X(t) . A generalized clause is of the form: 'Vx.C where C is a generalized formul;~. of the form V?= 1 P; (where P; are generalized literals and x a n-uple, possibly empty, of variables of order 1. A genemlized sequence is a finite sequence of generalized formulae. The set of instances of S is the set of sequences of clauses Su such that u is a ground substitution of Var(S).

3 An order among formulae

Before presenting our method we must clarify the notion of generalization and give a precise definition of it . A def­ inition of this notion was given in [Bourely et al., 1996] . We give here a new refined definition of the generaliza­ tion order that takes into account the semantic aspect of the clauses (i .e. the set of ground clauses denoted by the set) rather than its syntax.

The underlying ideas of this ordering are the following. Informally, a given theorem S will be said to be "more general" than .a theorem S' iff the hypotheses of S are weakerthan the one of S' or if the conclusion of S is stronger than the ones of S'. Indeed, it is obvious that S provides more. information than S'. If sets of clauses are considered, ·we set of hypotheses is the set of clauses S itself, and the conclusion is 0 (the empty clause) . Hence S will be more general than S' iff each clause in S belong to S', i.e. if S ~ S'. However, what is important here is not the sets of clauses S and S' by themselves but rather the set of ground clauses they denote. Therefore, we must take into account the two following possibilities:

1. The set of clauses S' does not explicitly contain S but any ground clause denoted by S belongs to the set of ground clauses denoted by S', i.e. S(S) ~ S(S'). In this case S can be said to be "more general" than S'.
2. C E S(S) and C rf. S(S') but C is S!fbsumed by a clause C' in S(S'). ·

In order to capture these two cases we introduce the following relation ~ bE.tween sets of clauses.

Definition 1 let S and S' be sets of clauses. We note S ~ S' iff for all C E S(S) there exists C' E S(S') such that C' ~. C.

Lemma 1 If S ~ S' then S' F= S.

Proof 1 Assume that S ~ S'. Let I be a model of S'. By definition if C E S(S') then I f= C. Let DES. We have S ~ S' hence by definition there exists C E S' such that C ~ D . IF= C (since C E S') hence If= D.

An unsatisfiable set of clauses S is said to be more general than S' iff S ~ S 1 . A satisfiable set of clauses S will be said to be more general than S' iff the hypotheses of S are stronger than the one of S' (this implies that S is false in more interpretations than S'). Consequently a satisfiable set of clauses S will be said to be more general than a set S' iff S' ~ S.

. Please note that these two notions of generalization are not equivalent. The following definition formalizes this idea.

Definition 2 Let T1 and T2 be two sequences of sets of generalized clauses. T1 is said to be more general than T2 (noted T1 ~ T2) iff for all substitution u2 ofVar(T2) , there exists a substitution u1 of Var(T1 ) such that

• T1 is unsatisfiable and T1 u1 ~ T2u2
• T1 is satisfiable and T2u2 ~ T1 u1.

Proposition 1 ~ is a pre-order.

Example 1 Lett1 : \fx .P(x)/\·P(a) , t2: P(a)/\·P(a). t 1 and t 2 are two unsatisfiable sets. The set of ground clauses denoted by t 1 and t 2 are respectively {P(t)jt E r(~ , V)} U {·P(a)} and {P(a),·P(a)}. We have t2 ~ t1 , hence t2 is more general than t1.

Example 2 Let t 1 : \fx .P(f(x )) 1\ ·P(a) and t 2 : P(f(a)) 1\ ·P(a) . t1 and t2 are satisfiable. We have t 2 ~ t 1, hence t2 is less general than t 1. t 1 is indeed falsified by more interpretations than t 2 (any model oft1 is a model oft2).

4 Matching

We call "matching" the process of finding-in the knowl­ edge base the formulae analogous to a given target for­ mula. It is inductively defined as follows .

Definition 3 A matching problem is of the form t = s (where t and s are terms or formulae), S ~ S' (where S and S' are sets of clauses), C ~. C' (where C, C' are clauses), :FVQ, :F 1\Q, \fx .:F, 3x .:F, where :F,Q are matching problems.

In order to give a semantics to matching problems we only have to choose the semantics of atomic formulae.

Definition 4 Let :F be a matching problem and let I be an interpretation. A substitution u is a semantic solu­ tion of :F w. r. t. I iff:

• :F is of the form t = s (where t, s are terms) and IF= tu = su.
• :F is of the form ¢ = 'lj; (where ¢, 'lj; are formulae) and I f= ¢u {::} 'lj;u.
• :F is of the form sl ~ s2 and there exists a set of clauses S3 such that S3 ~ S2u and If= (S1u ¢:} SJ) .
• :F is of the form C ~. D and there exists a clause C' such that C' ~. Du and If= (Cu {::} C').

The set of semantic solutions of P w. r. t . I is noted Sr(P).

Notice that the semantics of matching problem takes into account the semantics of the sets of clauses rather than their syntax. This is very important since analogy must focus on the semantic information contained in a theorem rather than in its statement.

Let Ss, ST be two sets of clauses. Finding a substitu­ tion u such that Ssu ~ ST (unsatisfiable case) or ST ~ Ss'u (satisfiable case) is equivalent to finding a solution of the matching problem Ss ~ ST (unsatisfiable case) or ST ~ Ss (satisfiable case). Both cases are noted Prob(Ss , ST) in the following.

Obviously finding the solutions of a matching problem is undecidable hence we cannot hope to get a general so­ lution to this problem. In the present paper we only give a set of rules allowing to find the solutions of some matching problem. We do not specify here the strat­ egy guiding the application of the rules (several different strategies can be proposed) . These rules are sound: any solution of the obtained problem is a solution of the ini­ tial one. However they are obviously not complete.

Matching problems transformation rules

Clausal transformation rules

Higher-order unification rules

The following rules are simply the standard higherorder unification rules (see [Huet, 1975]) .

Imitation

where X; (1 ::=:; i ::=:; n) are new free variables.

{X(t1 , ... , tn) = x}

Projection

Replacement

V-Elimi~ation rule

P V Q --+ P If P, Q are two matching problems.

Matching rules

The following rules are new. They allow to eliminate the symbols ~ and :=:;, from matching problems.

C:-Elimination rules

-c:-E1 51 u 52 c: 5 C-E2 0 c 5 - C-Ea 5C 0 ~-E4 {'fi.C} ~ 5 ~-Es {C} ~51 u 52 --+ ~-E6 {C} ~ {D} ~-E1 {AvB}~5 :::; ,-Elimination rules --+ --+ 51 ~51\ 52~ 5 T 5=0 VX.({C} ~ 5) {C} ~51 v{C} ~52 D <, C {A}~ 5v{B} ~ 5 :::; . -E1 C :::::; . '<fy.D --+ Vy.(C $. D) <,-E2 Vx.C < , D --+ 3x.(C :::::;. D) ~.-E4 C :::::; . Ih v D2 --+ (C :::::;. C!) v (C :::::; . C2) <.-Es .1. <, C --+ T ~ .-Es P ~ . Q --+ P = Q :::; .-E1 c1 v c2 :::;. D --+ c1 :::::; . D 1\ c2 :::::; . D

Next example illustrates the application of these trans­ formation rules :

Example 3 Let the source theorem be the set of clauses Ss = {c1 ,c2,c3} with c1 = Vx .P(x)VQ(x), c2 = ...,P(A), c3 = ...,Q(A) and the target theorem be the set of clauses ST = {c4 , cs} , where c4 = Vy.l(f(y)) V l(y) and cs = 'v'y . ...,l(y) . We solve the matching problem 'P: Ss ~ ST ? Remark: P, Q, A denote variables (of order 2, 2, 1 respectively) and l,f denote constant symbols (of order 2, 1}. .

We obtain a solution of the initial problem:

Remark: of course, other solutions could be obtained.

5 Lemma generation

In this section we identify a class of matching problems from which the solutions can be obtained automatically and we show how the proof (resp. the counter-example) of the target theorem can be automatically built from the one of the source (non-)theorem. In most cases, anal­ ogy will not directly give; a proof (counter-example) of the target formula from the source formula . Our method can cope with this case by generating lemmata that have to be proved in order to complete the proof/counter­ example of the target theorem. This is done by per­ forming a partial resolution of matching problems. We do not solve the problem completely, but only partially. Formulae that cannot be matched correspond to addi­ tional hypotheses that must be proven in order to com­ plete the proof or the counter-example. The derivation can then be completed in two different ways . Either by proving the lemma using a theorem-prover or by a re­ cursive call of the matching method ( unsatisfiable case) . Or by showing that the lemmata are compatible with the target set, i. e. that the adcling of those lemmata to the set preserves satisfiability of the set (satisfiable case).

A matching problem is in normal form iff it is of the form P : 1\~=l Xi = ti 1\ :F = _l , where , for all i ::; n, Xi occurs once in P and :F is a first-order formula. The formula :F corresponds to a formula that cannot be matched. We define new rules in order to generate problems in normal form.

Lemma generation rules

'<fy.(C = .1.) --+ ('<fy.C) = .1. 3y.(C=.l.) --+ (3y.C)=.l. C=.l./\D=.l. --+ CVD=.l. C=.l.VD=.l. --+ C/\D=.l. C=TVD=T --+ CVD=T C=T/\D=T --+ C/\D=T :F = .1. --+ -.:F = T 5=0 --+ S=T

We note matching the system composed by the uni­ fication and matching rules, the usual transforma­ tion rules for equational problems (see for exam­ ple [Comon and Lescanne, 1989; Lugiez, 1995]) and the lemma generation rules.

Theorem 1 (Soundness) Let P -+matching P'. For all interpretation I, Sz(P') ~ Sz(P) .

Theorem 2 Let Ss be a generalized sequence and Sr a set of clauses. Assume that Prob(Ss, Sr) -+matching P 1\ :F = .l. Let u be a solution ofP.

1. If Ssu is unsatisfiable and if for every interpretation I, I f= Sr => I f= ....,;: u, then Sr is unsatisfiable. On the other hand, there exists an algorithm that computes a refutation of Sr from a refutation of Ssu and :Fu 1\ Sr.
2. If Ssu is satisfiable and if there exists a model I of Ssu such that I f= -,:f'u, then Sr is satisfiable and I f=Sr.

In both cases, satisfiability or unsatisfiability of Sr is deduced straightforwardly from the one of Ss. To show that :F u is false in all models of Sr amount to prove that :Fu 1\ Sr is unsatisfiable. We can therefore use whatever theorem prover to prove that. The proof can also be ob­ tained with a recursive call of the procedure of analogy­ proving. If the source formula is satisfiable, one must (according to theorem 2) find a model I of Ss falsifying :Fu. In this aim, we try to find an extension of the (par­ tial) model of Ssu falsifying :F u. The difference with the unsatisfiable case is that the considered interpretation I is unknown a priori before the beginning of the search. In both cases, the derivation leading to the empty clause (resp. to a model) from the target set of clauses can be rebuilt straightforwardly from the source derivation and the proofs (or counter-example building) corresponding to :F.

Example 4 Consider the formula Ss and Sr of Exam­ ple 3. Once we have found the solution u of the problem Ss ~ Sr, it suffices according to theorem 2 to instantiate the proof of Ss in order to obtain a proof of Sr.

Now assume that we replace clause c4 in Sr by: cs = 'Vy.l(f(y)) V l(y) V l(g(y)). In this case the literall(g(y)) cannot be matched by the algorithm. If we apply the matching problem transformation rules, we get the prob­ lem in normal form:

In order to rebuild the ptoof of Sr we only have to prove the lemma: 3y . ...,l(g(y)), i.e. to prove that Sr u{l(g(y))} is not satisfiable. Any theorem prover can do that.

6 Examples

In this section we give two more realistic examples.

Example 5 (Unsatisfiable set of clauses) Let us consider the problems SYN310-1 and SYN312-1 of TPTP [Suttner and Sutcliffe, 1996].

Problem Ss zs: ...,p(x2, xl, x) V p(x , xl, x2) ...,p(xl,x,x2) V p(x ,xl , x2) ...,p(x,xl,g(x2)) V p(x, x l, x2) ""P(f(x ), xl, x2) V p(x, xl, x2) ...,p(a, b, c) p(f(g(a)), f(g(b)) , f(g(c))) Sr is: p'(x, x3, x2) V ...,p'(x, xl, x2) V ...,p'(xl, x3, x2) p'(x2, xl, x) V ...,p' (x, xl, x2) p'(xl, x, x2) V ...,p'(x, xl, x2) p'(x, xl, f'(x2)) V ...,p'(x, xl, x2) p'(g' (x ), xl, x2) V ...,p'(x, xl , x2) p'(a', f'(b'), c') p'(f'(b'), d, c') ...,p'(g'(f'(a')), g' (!'(d)), g' (f'(c')))

S s is very easy (it can be proven in 0.17 seconds by OTTER 3.0 [McCune, 1995] with "automatic" mode). Sr is more difficult (OTTER takes 536.31 s to prove it in automatic mode). We assume that a proof of Ss is known and we try to build automatically a proof of Sr by analogy with the one of Ss .

We apply our algorithm in order to solve the problem Ss ~ Sr? No general solution can be found. Indeed Sr is not a direct instance of Ss. However we get the follow­ ing partial solution: {p= >.xl,x2,xs . ...,P'(xs,x2,xl),g = >.x .f' ( x), f = >.x .g' ( x), a = a', b = b', c = c', d = d'} with the lemmata:

These two formulae are clauses belonging toSs that can­ not be matched by Sr.

According to Theorem 2 it only remains to prove the lemmata. The first one can be proven (very easily) by adding the negation of p'(a, b, c) to Sr (OTTER takes 0.37 s to prove it).

In order to transform the second lemma into a set of clauses we need to use skolemization. We get { ....,p'(al, a2, as), p'(a1, as, a2)}. This set is added to Sr . The corresponding set can again be proven very easily (OTTER takes 0.18 s).

This example suggests that reasoning by analogy can enhance significantly the power of theorem-provers. In­ deed the total amount of time required to prove the lem­ mata is 0.55 s and the time required to prove the whole theorem without using analogy is 536.3ls . Please note that the proofs of the lemmata does not require any user­ interaction. However the matching process is not yet implemented, hence must be done by hand.

E~ample 6 (Satisfiable set of clauses) Let Ss be the following satisfiable set of clauses (adapted from [Church, 1940]).

The finite model builder FMC developed in our infer­ ence laboratory builds the following model (in 0.01 s) .

Hodel:

Now, let Sr be the following set of clauses {--,f'(x) V ..,(f'(y'(x))),f'(x)Vf'(y'(x)))} . Here, if we replace f',y' by / , y, we have obviously Ss f= Sr. Hence we try to build a model of Sr by analogy with the one of Ss . We first solve the matching problem: Prob(Ss, Sr) = Sr !; Ss. We obtain the following solution: y = .Xx .y'(x), f = >.x.f'(x), with the lemma: \fx .p(x) V --,p(x) . According to theorem 2 it only remains to check if the lemma holds in the model of Ss . This is obviously the case since Vx .p( x) V """'P( x) is a tautology. Therefore the following interpretation is a model of Sr : {!'(0) = true,f'(1) = false,y'(O) = 1,y'(1) = 0}.

7 Discussion and perspectives

We have presented a calculus for the discovery and han­ dling of analogy between sets of clauses. It is able in par­ ticular to handle partial analogy between statements by generating lemmata. Our work is the first step toward a system for simultaneous search for refutations and mod­ els using analogy and abductive reasoning. Main lines of future research are:

• Define strategies or heuristics for our calculus matching and study their properties (termination, efficiency, completeness for some classes of problems etc.).
• Extend this approach to first-order formulae (not in clausal form). In particular we have to give a new definition of the generalization order .

A comparative analysis with the lemmata produced by other techniques such as [Kolbe and Walther, 1995] will be performed in the future . We are currently working on the implementation of the calculus and on the definition of the knowledge base.

Acknowledgements

We thank Ricardo Caferra and the anonymous referees for their pertinent and precise comments.