Abstract Theorem Proving

1 Introduction

Abstraction has been suggested as a very powerful technique for constraining search in automated reason­ ing. Informally, abstraction can be described as the process of mapping a representation of a problem (also called the "ground" representation) into a new represen­ tation (also called the "abstract" representation) which preserves certain desirable properties and is simpler to handle. The "desirable properties" amount to requir­ ing that the abstract solution be of help in solving the problem in the original search space. The notion of "sim­ plicity" depends on the application, it may mean decid­ ability or lower complexity.

As far as we know, no comprehensive theory of ab­ straction has been given. The only work in this direction [Plaisted, 1981] is concerned with one form of abstraction and is limited to the area of resolution theorem proving. This has caused the lack of a satisfactory characteriza­ tion and general understanding of abstraction.

The aim of the work (partially) described in this paper is to provide a theory of abstraction and use it to: (1) understand what "to abstract" means and how it can be formalized; (2) classify the various forms of abstraction; (3) investigate their formal properties and the opera­ tions which can be defined on them; ( 4) analyze and classify past work; (5) define ways of building "useful Toby Walsh Department of Artificial Intelligence University of Edinburgh 80 South Bridge, Edinburgh Scotland Toby_ Walsh@uk.ac.edinburgh abstractions" and (6) study how the proof in the ab­ stract space can be used to aid the proof in the ground space.

"This work was begun when the first author was working at the Department of Artificial Intelligence at Edinburgh Uni­ versity supported by SERC grant GR/E/4459.8. The second author is supported by a SERC studentship. The research described in this paper owes a lot to the openess and sharing of ideas which exists in the Mathematical Reasoning group. The authors thank Alan Bundy, Enrico Giunchiglia, Alex Simpson and Richard Weyhrauch for the many discussions on the topic. Alan Bundy is also thanked for reading early versions of the paper.

In this paper, for lack of space, only some issues are discussed and proofs are only outlined and the sim­ plest not given (for a more complete treatment see [Giunchiglia and Walsh, Forthcoming 89]}. Only top­ ics (1), (2), (3) and (4} are (partially) dealt with. The following of the paper can be structured in three main parts.

In the first part (section 2), the formal framework is presented and some of ·the underlying motivations are discussed (topics (1) and (2)). Abstraction is first de­ fined as a mapping between formal systems and then classes of abstraction are identified depending on how certain properties ( ie. provability, inconsistency) are preserved by the mapping.

In the second part (section 3), some examples/ case studies of previous work in abstraction are presented [Sacerdoti, 1974, Plaisted, 1981, Hobbs, 1985] (topic (4)). The goal here is to motivate the formal framework by showing how it can be used to capture and formalise most of the relevant previous work in various areas of AI 1 . This allows us to get an unified view of work which, on the surface, seems very different. For instance it is proven that the theory of granularity presented by Hobbs in [Hobbs, 1985] and described in example 3 can be for­ malised as a particular case of the weak and ordinary abstractions defined by Plaisted in [Plaisted, 1981] and described in example 2.

In the third and last part (section 4}, it is then shown how the framework can be actually used to understand the properties of abstraction mappings and to find solu­ tions to existing problems (topic (3)). In particular the "false proof problem is investigated. Intuitively stated, the false proof problem is as follows . In order to build an abstract space "simpler" than the ground one, the trick is to forget some "irrelevant" details 2 · This, Plaisted noticed [Plaisted, 1981], may cause problems. In partic­ ular the abstract space may be inconsistent even if the ground space is not. It is proven that this problem can­ not be avoided as it is always possible to find a set of consistent axioms whose abstraction is inconsistent. A solution is then proposed based on the ordering of ab­ stractions into a partial order.

1 This case study analysis is performed in much more depth in [Giunchiglia and Walsh, Forthcoming 89]; in [Giunchiglia and Walsh, 1989] it is shown how the framework can be ef­ fectively used to build global strategies for the unfolding of definitions.

2 Where "irrelevant" should be read as "irrelevant accord­ ing to same theorem proving strategy".

2 The formal framework

Definition 1 (Formal system) : A formal system E is a triple (A, 1:::,, 0), where A is the Language, 0 is the set of axioms and /:::, is the Deductive Machinery of E.

The language A is composed of an alphabet, the set of (well formed) terms and the set of well formed formu­ lae (wffs from now on). 0 is a subset of the wffs of A. The deductive machinery is a set of rules of inference for deriving theorems from axioms.

Definition 2 (Abstraction} /fE1 = (Ar; 1 ,0r; 1 ,/:::,r; 1 ) and E2 = (Ar: 2 , Or: 2 , /:::,r; 2 ) are two formal systems, an abstraction mapping f, written also f : E1 1--+ E2, is a triple of total functions (fA, fo, h) suck that:

If not explicitly stated to the contrary we assume that fA and fo agree on the axioms; that is, for any wff w, if wE 0, then fA(w) = fo(w) 3 · When no confusion arises we drop the subfixes. Given a deduction tree Ilr: 1 of 1--r: 1 <pr; 1 in E1, we indicate by f(IIr:.) a deduction tree IIr:, of 1--r:, f(<pr: 1 ).

Definition 3 (T*-abstractions} : An abstraction f : E1 1--+ E2 is said to be a 4

TC-Abstraction iff, for any wff <pr; 1 , 1--r: 1 <pr; 1 iff 1--r:, f ( <pr:.);

TD-Abstraction iff, for any wff <pr; 11 ifl--r: 2 f(<pr: 1 ) then 1--r: 1 <pr: 1 ;

TI-Abstraction i[f, for any wff <pr; 1 , ifl--r: 1 <pr: 1 then 1--r:, f ( <pr;.).

It can be easily proved that any TC-abstraction is both a TD-abstraction and a Tl-abstraction.

We write "T*-abstraction" to mean any of the above abstractions, TH(E) to mean the set of wffs provable in E and NTH(E) to mean the set of wffs which, if added to the axioms of E, make it inconsistent.

TC-abstractions map all the elements of TH(EI) into elements of TH(E2) and these are all and only the ele­ ments of TH(E2). Herbrand's theorem [Goldfarb, 1971] can be formalized as a TC-abstraction. TC-abstractions are used, for instance, in decision theory, under the name of reduction methods, to prove the decidability of and to build deciders for the validity problem for certain sub­ classes of the first order calculus [Dreben and Goldfarb, 1979]. The trick is to find a class whose decidability is known and prove that there is a proof of a wff iff there is a proof of the "translated" wff in the new class.

3 To be precise, since we distinguish between wffs occur­ ring as axioms and as anything else, we should consider oc­ currences of wffs and not wffs. Since, in this paper, for any wff w, if wE 0, then /A(w) = fo(w), to make things simpler, we consider !A and f !!>. to range over wffs.

4 "T" stands for theorem, "C" for constant, "D" for de­ creasing and "I" for increasing.

In TD-abstractions a subset of the elements of TH(EI) is mapped into TH(E2) and these are all the ele­ ments of TH(E2). TD-abstractions are used, for in­ stance, to implement derived inference rules [Giunchiglia and Giunchiglia, 1988] and, as alternatives to Tl­ abstractions, to overcome some of their problems [Tenen­ berg, 1987] (see later).

In Tl-abstractions all the elements of TH(Ei) are mapped into a subset of TH(E2). Tl-abstractions have been mostly used in "abstract theorem proving" (see fig­ ure 1). The main idea underlying the use of these abstractions is to prove the abstracted theorem in E2 (which, supposedly, should be simpler than in Ei) and then to use the structure of the proof in E2 to shape the proof in E1. The fact that there is a proof in E2 does not guarantee that there is a proof in E1 ·

T*-abstractions are classified on how provability is preserved between the ground space and the abstract space; they are thus useful when the deductive machin­ ery is defined to generate theorems. On the other hand there are formal systems ( ie. resolution) whose deduc­ tive machinery determines inconsistency. In these cases, abstractions must be classified on how inconsistent for­ mal systems are mapped. This requires the definition of new classes of abstractions, called NT*-abstractions. Thus, for instance, NTI-abstractions are defined as follows 6 :

Definition 4 : An abstraction f : E1 1--+ E2 is an NTI­ Abstraction iff, for any wff <pr; 1 , if adding <pr; 1 to the axioms of E1 yields an inconsistent formal system, then adding f(<pr: 1 ) to the axioms ofE2 yields an inconsistent formal system.

Various properties, equivalences, and relationships among T*- and NT*-abstractions can be proved [Giunchiglia and Walsh, Forthcoming 89]. NTI­ abstractions' behaviour can be represented as in figure 2.

In this paper we mention only one result which allows us to prove how and to what extent T*-abstractions (and in particular Tl-abstractions) can be used in resolution based theorem provers. Note that, if a formal system E has negation, then, for any wff a, a E T H(E) iff -,a E NT H(E). Thus trivially:

Corollary 1 : If E1 and E2 are two formal systems with. negation and if f : E1 1--+ E2 is a Tl-abstraction then, for any a, if a E TH(Et) then -,a E NTH(E!) and -,f(a) E NTH(E2).

6 NTC-abstractions and NTD-abstractions are defined analogously to TC-abstractions and TD-abstractions respec­ tively, but preserving inconsistency instead of theoremhood (see definitions 3, 4).

Tl-abstractions can be used in resolution theorem prov­ ing as long as, in the abstract space, the wff added to the axioms is the negation of the abstraction of the wff whose negation is added to the axioms of the ground space. This makes Tl-abstractions very useful since often refu­ tation systems, take as input a goal formula a (usually automatically) negate it, add the result to the axioms and try to prove that the resulting theory is inconsis­ tent. In the abstract space, instead of /(-,a), -,/(a) is added as an axiom.

On the other hand there are Tl-abstractions which can be used in resolution-based systems independently of whether the negation in front of the goal is abstracted.

Definition 5 (Negation preserving) : An abstrac­ tion f: E1 1-+ E2 is negation preserving iff f(-,a) = -,f(a).

Theorem. 1 : If E1 (A1, 01, ..6.1) and E2 (A2, 0 2, ..6.2) are two formal systems with negation, then a negation preserving abstraction f : E1 1-+ E2 is a Tl-abstraction iff f' : E~ 1-+ E~ is a NTI-abstraction, where E~ =(All 01, t!.D, E~ = (A2, 0 2, fl.~) and fl.~ and fl.~ are such that TH(Ei) = TH(E1) and TH(E~) = TH(E2) .

Examples are / = /' with Ell E2, E~ and E~ being natural deduction, and f =/= f' with E1, E2 being natu­ ral deduction and E~, E~ being resolution. As far as we know, all the abstractions proposed to work in resolution systems are negation preserving. However, there are use­ ful abstractions which are not negation preserving (for instance when negation is not part of the language of E1 or E2 [Newell et al., 1963], or only partially preserved by the mapping) .

3 Some examples of abstraction

The purpose of these examples, together with provid­ ing a rational reconstruction of the work described, is to convince the reader that the framework is very power­ ful and allows us to present an unified view of the work done in different areas and with different goals. For lack of space, only three examples are reported, more "histor­ ical" examples are reported in [Giunchiglia and Walsh, Forthcoming 89].

EXAMPLE 1 [Planning]: Abstrips [Sacerdoti, 1974] was one of the first noticeable applications of abstrac­ tion. In Abstrips the preconditions to operators were abstracted according to their criticality. To formalize Strips-like planning we shall adopt a situation calculus in a natural deduction formal system. Let us consider the abstraction f AB where E1 and E2 are situation cal­ culi with a first order language, 0 consists of frame, op­ erator and theoretic axioms and fl. consists of natural deduction rules of inference. Operators are wffs of the form " Vs.(/\1<i<n Pi(s) ---. q(f(s))) " where Pi is a precondition, s-is-a state of the world, f is some action, and q describes the new state of the world. Goals are wffs of the form "3s r( s )". f AB is applied to wffs and axioms as follows:

!AB(a) =a if a is an atomic formula.

fAB(-,a) = -,fAB(a);

!AB(aof3) = fAB(a)ofAB(/3), where "o" is "A" or "V";

!AB(Ux a)= Ux !AB(a), where "U" is "3" or"'</";

IAB(a---. /3) = !AB(a)---. !AB(/3), provided "a---. {3" is not an operator;

fAB(I\1~i~n Pi(s) ---. r) = /\iEcrit(~e) Pi(s) ---. fAB(r), providedthat"/\1<i<nPi(s)---. r" isanoperator,where i E crit(~t) if the criticality of Pi is greater than 1t.

Theorem. 2 : !AB is TI, namely, i/f-r: 1 cpr; 11 then f-r:, fAB(IPr:l).

Proof!Outline]: By proving that given a deduction tree Ilr: 1 ot f-r: 1 cpr; 1 , we can build a deduction tree Ilr:, = !AB(IIr:J off-r:, !AB(IPr: 1 ). The proof proceeds by in­ duction on the weight N 6 of Ilr:.J. For proofs of weight 1, f AB is applied to the single wtt; this generates a valid proof in Ilr:,. Assume that we have a deduction tree up to weight N. Any rule application that is not modus po­ nens involving an operator translates unmodified, in the sense that, for instance, an "VI" on cp in Ilr: 1 becomes an "VI" on f AB ( cp) in Ilr:~ . For an operator application, the following transformat10n is performed:

The abstract proof is valid since !AB(. .. ) is a valid deduction tree from the induction hypothesis, and the hypothesis of the (abstract) operator axiom is obtained from "/\1<i<nPi" by a (possibly empty) sequence of ap­ plications -of "and-elimination". D

Note that the abstract proof is longer than the one in the ground space. The purpose of abstracting is not to find these longer proofs; we hope that there are also go­ ing to be shorter proofs. These shorter proofs are those that don't try to satisfy p · for j ¢ crit(~t). There is no guarantee that there witl be a shorter proof than the one exhibited; we will always be able to devise an obtuse theory in which to prove the Pi for i E crit(~t) we have to prove all the other P; for j ¢ crit(~t). ·

6 The weight of a deduction tree is the number of its for­ mula occurrences.

EXAMPLE 2 [Resolution theorem proving, logic pro­ gramming]: The work by Plaisted is closest in spirit to ours. Plaisted proposes two classes of abstraction, ordi­ nary abstractions and weak abstractions [Plaisted, 1981], which map a set of clauses onto a set of clauses and pre­ serve inconsistency. His work is less general than ours as: he restricts his attention to resolution systems and his classes of abstraction fail to capture all NTI-abstraction mappings that preserve inconsistency between resolution systems. In other words, Plaisted's abstractions are NTI, but not all NTI-abstractions are weak or ordinary 7 . Moreover we claim that our definitions of abstraction are "more natural" in the sense that better reflect and capture the functionalities they are given for.

Ordinary abstractions are described as taking both E1 and E2 to be first order calculi with Ar: allowing clausal form, .!lr: being resolution and Or: being arbitrary. Any ordinary abstraction mapping f maps a clause in Ar: 1 onto a set of clauses in Ar: 2 subject to the following con­ ditions:

1. /{1.) = {..l};
2. if a 3 is a resolvent of a1 and a2 in E1, and {33 E /(a3) then there exist P2 E j(a2) and fJ1 E f(ai} such that a resolvent of {31 and fJ2 subsumes {33 in E2;
3. if a 1 subsumes a 2 in E1, then for every P2 E !(a2) there exists {31 E f(ai) such that P1 subsumes P2 in E2.

Weak abstractions are identically defined to ordinary abstractions except condition b) is weakened to the property that if a 3 is a resolvent of a 1 and a2 in E11 and {33 E f(a3) then there exist fJ2 E j(a2) and fJ1 E f(a!) such that either fJ1 subsumes {33, or fJ2 subsumes {33, or a resolvent of {31 and {32 subsumes {33 in E2 ·

Theorem 3 : Weak and ordinary abstractions are NT!.

Proof: The proof is a corollary to Theorem 2.5 on page 55 of [Plaisted, 1981]. 0

Theorem 4 : There exist NTJcabstractions between res­ olution systems that are not weak or ordinary abstrac­ tions.

Proof[Outline]: We can find NTI-abstractions that fail every one of the three conditions in the definition of weak and ordinary abstractions. Condition a) is failed by the NTI-abstraction f such that, for any wff cp in E1, f( cp} = { cp V ..l}. The problem with condition b) is that we may also need to resolve with an axiom of the the­ ory. Consider, for instance, the abstraction defined by f(p V q) = {p V r} and f(cp) = {cp} otherwise. If E1 contains the axioms, ·q, and ·r then f is NTI. In par­ ticular, p V q resolves with ·p in E1 to give 9· However, no clause in the abstraction of p V q, or ·p (or their re­ solvent} subsumes the clause q found in the abstraction of q. For condition c), consider the abstraction defined by f(p V q) = {r, p V q} and f(cp) = cp otherwise. Now f is NTI. However, f fails condition c) of the definition of weak and ordinary abstractions as p subsumes p V q but no clause in the abstraction of p subsumes r which is in f(p v q). 0 .

7 All Plaisted's examples of abstraction are negation pre­ serving and thus also TI.

The definition of weak and ordinary abstractions could be extended to overcome the first counter-example by re­ placing condition a) with the more general requirement that 3cp E /(..l}. 1-r: 1 ·cp. However, this still leaves use­ ful NTI-abstractions that fail conditions b) and c). For example, if Po +-+ Pi for many i we might abstract many clauses of the form p,Vq onto the one clause {pVq}. One could argue that ordinary and weak abstractions have the advantage, over NTI-abstractions, that they always map into simpler theories, in the sense that there is al­ ways an abstract proof that is no longer than the short­ est proof of the unabstracted theorem [Plaisted, 1981]. This does not seem a good point since, first of all, we intuitively expect NTI-abstractions (that are not NTC) to have this or similar properties and, second and more importantly, there are NTI-abstractions, which are not weak or ordinary, which build simpler theories (the last example is one possible case). ·

EXAMPLE 3 [Common sense reasoning]: In [Hobbs, 1985], Hobbs presents a theory of granularity in which a complex theory is abstracted onto a simpler, more "coarse-grained" theory with a smaller domain; for ex­ ample, we could map the real world of continuous time and positions onto a (micro}world of discrete time and positions. Hobbs' granularity theory can be formalized as a mapping (let us call it "/gran"} that can be proved to be TI. Let us suppose that both E1 and E2 are cal­ culi with a first order language, an arbitrary set of ax­ ioms and any complete deductive machinery for first or­ der logic. /gran maps different objects in E1 into (not necessarily different) objects in E1 according to an in­ di~tinguishability relation, defined by the (second-order) ax1om:

where R is the subset of the predicates of the theory determined to be relevant to the situation at hand 8 · Thus /gran keeps the same logical structure of wffs and translates any constant into its equivalence class, namely /gran(p(a}} = p(~t(a}) where a is any constant symbol and ~t( a) is the equivalence class of the constant a wrt the indistinguishability relation; that is ~t(x} = {y: x ""'y}.

Theorem 5 : /gran is TI/NTI.

Proof By mapping a proof tree 1Ir: 1 in E1 of cpr: 1 (pos­ sibly of ..l} onto a proof tree 1Ir: 2 in E2 of f(cpr:J. The proof proceeds by induction on the weight of 1Ir: 1 · We merely apply fA to every wff in 1Ir: 1 · 0

(Like any TI abstraction, see next section} /gran can map a consistent theory into an inconsistent theory. For ex­ ample, if the constants a and b are "indistinguishable", then a consistent theory with equality and the axiom ·(a =b) maps into an inconsistent theory with the ax­ iom ·( {a, b} = {a, b}). However, the following result holds:

Theorem 6 : fv.ran preserves consistency if indistin­ guishability is dejtned over all predicates.

8 As in [Hobbs, 1985], we define indistinguishability for unary predicates; it can, however, be easily generalized to n-ary predicates.

Proof[Outline]: By contradiction. Assume that a con­ sistent theory, 'E1 maps onto an inconsistent theory, E2. That is, we can find a proof tree, ITE 2 of .L We show how you can construct a proof tree, ITE 1 of .l, contradicting the assumption that E1 is consistent. For every equiva­ lence class, ~~:(a) we pick one member of that class, b; to every wff, cp in ITE 2 we apply the substitution {~~:(a)(b}. This will generate a proof tree, nE. whose assumptions will either be axioms ofE1 or will be derivable from them using the indistinguishability relation and substitution of equivalences. If indistinguishability is not defined over all predicates, this last fact will not necessarily be true. 0

Note that luran is a special case of the example of weak/ ordinary abstractions (given in [Plaisted, 1981]) where function symbols are renamed in a systematic (but not necessarily 1-to-1) way. ·

4 The false proof problem

A major problem with the use of Tl-abstractions 9 is that, even if E1 is consistent, E2 may be inconsistent. An example has already been given for luran· With f AB it is sufficient to consider abstracting the operators "a1/\ a2 -+ a3" and "a1 A a4 -+ --.a3" onto "a1 -+ a3" and "a1 -+ --.a3" when a 1 is a theorem but a2 and a 4 are not both theorems. This problem was noticed by Plaisted [Plaisted, 1981] who called it the "false proof problem". A symptom of the problem comes from the following theorem:

Lemma 1 : Iff : E1 1-+ E2 is an abstraction and E2 is inconsistent then f is a TI-abstraction.

Lemma 1 holds independently of the consistency of E1. Example can be easily found with E1 consistent or with E1 inconsistent. Once f has been proved to be TI it may happen that E2 is inconsistent. This is a major blow to the use of TI-abstractions to guide the proof in the ground space. When E2 is inconsistent the structure of the proof in E2 could still be used to shape the proof in E1. However, any wff in E2 is a theorem and thus E2 does not filter out any of the wffs which are not theorems in E1. In a way E2 gives too little information. To make matters worse, in general it is not possible to decide in a finite amount of time whether a formal system is consistent.

When working with a fixed formal system ( ie. set theory+ first order logic) a solution is to build abstrac­ tions which are proved a priori to have consistent E2. In many cases, however, ( ie. planning, logic program­ ming, knowledge based systems), while the set of infer­ ence rules of E1 is fixed, its axioms may vary and de­ pend on the application. Tenenberg [Tenenberg, 1987, Tenenberg, 1988] proposed some solutions to the prob­ lem for predicate abstractions 10 in a resolution-based system. However, the abstractions he proposes have many drawbacks: in one case the abstraction is TI but OE 2 is not recursive (even if recursively enumerable) and it may take an infinite amount of time to generate it; the other two types of abstraction are TD or similar to TD [Giunchiglia and Walsh, Forthcoming 89] 11 . This means that completeness is lost since there is at least one theo­ rem in E1 whose abstraction is not a theorem in E2. We consider completeness the one property you do not want to lose.

11 Everything stated in this section holds dually for NTI­ abstractions.

10 Predicate abstractions are abstractions where distinct predicate symbols in 1:1 are mapped onto (possibly not dis­ tinct) predicate symbols in :E:z.

The ideal solution would be to generalize the concept of abstraction mapping to be parameterized on the ax­ ioms of E1 and then to find sufficient conditions which guarantee that a TI-abstraction maps E1 into a consis­ tent E2, independently of the axioms of E1 (as long as E1 is consistent). This seems a reasonable request since there are abstractions which, fix AE 1 , AE 2 , ilE 1 , ilE 2 fA, /o and fA are TI for any choice of the theoretic ax­ ioms (this is, for instance, true for the abstractions of the three examples) 12 . This request turns out to be unsat­ isfiable. In fact, even if there are abstractions which are TI- for any choice of the theoretic axioms, for any such TI-abstraction there always exists a set of consistent ax­ ioms whose abstraction is inconsistent. The argument goes as follows.

Let AE 1 and AE be two languages, ilE 1 and ilE 2 two deductive machineries. Then, if fA : AE 1 1-+ AE 2 , g : AE 1 1-+ AE 2 and fA : ilE 1 1-+ ilE 2 are three to­ tal functions, F = (/A, g, /A) is an abstraction from E1 = (AE 1 , AE 1 , LlE.) tq E2 = (AE~· AE 2 , ilE 2 ). Then for any OEl c AEl, if by "g i oE. we indicate g restricted to apply to oE., F 0 Dl = (fA, g i oE., fA) is an abstraction from E~Dl = (AE., oE., ilEl) to E~Dl = (AE 2 , OE 2 , ilE 2 ), with OE 2 = g(OEJ ·

Theorem 1 : Let AE 1 and AE 2 be two languages, ilE 1 and Llr: 2 two deductive machineries, fA : Ar: 1 1-+ Ar: 2 , g : AE 1 1-+ AE 2 and fA : LlE 1-+ LlE 2 three total functions . Then there exists oE. c AEl suck that, if the abstraction F 0 Dl = (fA, g i oE .. !A) is Tl and NTI but not NTC, k ~OD . · d ~OD1 · · · t en "-'1 1 IS conssstent an "-'2 IS 1ncons1stent.

Proof!Outline]: By constructing oE.· Because F 0 Dl is NTf- but not NTC-, there exists a wff cp such that adding F 0 D1 (cp) as an axiom to E2 makes an inconsis­ tent formal system, but that adding cp as an axiom to E1 doesn't. 0

Theorem 7 can actually be proved in more power­ ful forms; however the hypotheses hold for . most TI­ abstractions. For instance negation preserving abstrac­ tions that are TI are also NTI and vice versa (theorem 1) . Theorem 7 proves that we .cannot find a Tl-abstractions which maps a consistent E1 into a consistent E2 indepen­ dently of the axioms of E1. One possible solution is to define abstractions which ~uarantee to build consistent abstract spaces for certain lsyntatic characterisations of) classes of theories. However such a solution would not solve the problem in its generality and could not be used in a general purpose, theory independent "abstract the­ orem prover". A different approach is to be able to vary (in an automated way) the TI-abstraction until we can decidably show that E2 is consistent. This can be done as follows.

11 Note that it can be proved that, more generally, for any TO-abstraction, if :!::1 is consistent, so is :E:z.

12 0f course theory independent TI-abstractions are in gen­ eral less efficient than the ones geared towards one single the­ ory as they do not exploit the structure of theoretic axioms.

TI-abstractions applied to the same E1 can be classi­ fied into a weak partial order, indicated by "~".

Definition 6 (~) : If h : E1 ~ E~ and li : E1 ~ E~ a re two TI-abstractions then h ~ li iff for all wffs IPE 1 , if f-E' h(IPE 1 ) then f-E; 1i(IPE 1 ). We say that h is · · weaker than li or, dually, that li is stronger than fi.

If h ~ li, then li is stronger than h in the sense that there are fewer wffs which are theorems in E~ and not in E1 than wffs which are theorems in E~ and not in E1 · "~" is in general a weak partial order (respect­ ing transitivity, antisymmetry and reflexivity) but not a total order. If, however, we have a set of totally ordered abstractions then the following result holds:

Theorem 8 : If It : E1 ~ E~, ... , In : E1 ~ E2 are TI-abstractions and ft ~ ... ~In {ft, ... ,ln are totally ordered), then if E2 is consistent so is E~ for any 1 ~ i ~ n.

Theorem 8 suggests the following process:

• build sets of abstractions, F, = {If, ... , 1~,} where If ~ ... ~ 1~, and f~, (Et) is decidable ( eg. it is propositional).
• find a set, Fi in which the codomain of the strongest abstraction I~ . (Et) is consistent. Note that, since J I~; (Et) is decidable, its consistency or inconsistency can be proved in a finite amount of time.
• starting with the strongest abstraction (that is with l = ni), untill > 1 use the proof that the abstracted wff is a theorem in I{(Et) to help construct a proof in !{_1 (Et). If, in any of the I{(Et), the abstracted wff is not a theorem, then the wff cannot be a the­ orem in E1 (since 1/ is a TI-abstraction).
• when l = 1, use the proof in El to help construct the proof in E1. If success, then the goal is a theorem.

Of course there is no guarantee that all the steps in unab­ stracting back to E1 will go through or terminate. The overall performance depends on how the various abstrac­ tions in the total order are built and on how the process of unabstracting is performed. For instance, computing the consistency of I~ . (Et) can be optimized by build-' ing a very simple, "minimal" I{ (Et). Further time can J also be saved, when I~;(Et) is proved inconsistent by introducing (in an automated way) small variations in I~; that are tuned to the source of the inconsistency.

5 Conclusions

In this paper we have proposed a theory of abstraction which extends the notions of abstraction previously used. We have focused on abstract theorem proving and have suggested that a certain class of provability preserving abstractions 13 , TI-abstractions (which are not TC) are the correct abstractions to use. TC-abstractions are in general too strong, and the goal of having "simpler" ab­ stract proofs does not seem achievable except in very special and limited forms (for instance, if I : E1 ~ E2 is a TC-abstraction then if E1 is undecidable then E2 can­ not be decidable). The dual class of provability preserv­ ing abstractions, TD-abstractions (which are not TC) are of less use as they lose completeness; that is, there is at least one theorem whose abstraction is not a theorem.

13 Everything said in this section holds dually for NTI­ abstractions.

Unfortunately, TI-abstractions are subject to the false proof problem; they can map a consistent theory into an inconsistent abstract theory. This problem has been tackled in the last section, where a new general purpose solution has been proposed.