A Many-Sorted Calculus Based on Resolution and Paramodulation

1. I nt!toduc.tio n

Sorts are frequently used in practical applications of the first-order predicate calculus. For example we write formulas like

• (i) Vx:S. l(x) and 3x:S. I (x) and treat them 6o!tma.lly as a.bb!te.via.tionl.> for
• (ii) Vx. S(x) ~ l (x) and 3x. S(x) A l (x).

We use we.ll J.>oltte.d formulas because they provide a convenient shorthand notation for ordinary first-order formulas. But sorts also in6lue.nc.e. the. de.duc.tionl.> from a given set of well sorted formulas. For instance, if Pis a predicate only defined on thesort ~ of integers, we will never perform a deduction like Vx:7L P (x) f- P (~). Proofs are simplified, because a ma.ny-l.>oltte.d c.a.lc.ulu!.> is more adapted to a ma.ny-J.>oltte.d the.oltlj and hence not surprisingly de.duc.tionl.> whic.h lte.l.>pe.c.t I.>Oittl.> as well as the ul.>a.ge. o6 we.ll J.>oltte.d 6o1tmula.1.> reflect the everyday usage of predicate logic.

Let us sketch how a ma.ny-J.>oltte.d (mehrsortig) calculus is developed from a given (sound and complete) first-order one-sorted (ein­ sortig) calculus: Assume we have a set of l.>oltt l.>ljmbol!.>, ordered by a given J.>ubJ.>oltt O!tde.!t . Variable and function symbols (of our given calculus) are associated with a certain sort symbol. The J.>oltt o6 a. te.ltm is determined by the sort of its outermost symbol. In the construction of we.ll l.>oltte.d (sortenrecht) formulas, we only allow well sorted terms of a certain doma.inl.>oltt or of a J.>ubl.>oltt of this domainsort for each argu­ ment position of a function or predicate symbol.

The in6e.!te.nc.e. 1tule.1.> of the many-sorted calculus are the inference rules of the given calculus, but with the restriction that only we.ll l.>oltte.d 6o1tmula.1.> can be deduced by an application of the restricted inference rules. Starting with well sorted formulas this guarantees that only well sorted formulas are derived in a deduction in the many-sorted calculus.

Taking J. He.!tb!t a.nd!.> thesis [Her30] as the starting-point, various many-sorted versions of different first-order calculi have been proposed and investigated by A. Sc.hmidt [Sch38,Sch51], H. Wa.ng [Wan52], P.C. Gilmo!te. [ Gi 158] , T. Ha.ilpe.!tin [ Hai 57] , A. Obe.Mc.he.lp [Obe62] and A.V. Ide.l!.>on [Ide64].

The advantages of a many-sorted calculus are well recognized within the field of Automa.te.d Th e.olte.m Pltoving, e.g. [Hay71, Hen72]. Several theorem proving programs are also based on some kind of a many-sorted calculus, e.g. [Wey77,Cha78,BM79](unfortunate­ ly without a sound theoretical foundation) As a result of this the works cited above become of p~actical significance.

Most theorem proving programs are based on a first-order calculus whose inference rules are 6acto~ization, ~e~olution and pa~amodulation [Rob65, WR73] and whose formulas (called clau~e~) are in skolemized conjunctive normal form [Lov78]. We call such a calculus an RP-calculu~.

In this paper, we shall define the ERP­ calculu~, i.e. a many-sorted version of the RP-calculus, and we shall introduce a notion of E-unsatisfiability of sets of well sorted clauses, called EE-un~ati~6iability.

Obviously we are only interested in a many­ sorted calculus which is sound and complete, but in addition we can ask: Which formulas do we expect as theorems of the ERP-calculus compa~ed to those of the RP-calculus? To facilitate a comparison between both these calculi, we represent the relations between the function symbols and the sort symbols as well as the subsort order by the set AE of l.lo~t axiom~ (Sortenaxiome), i.e. a set of first-order formulas. For a well sorted formula <1>, as e.g. (i) above,the~elativization ~ (Sortenbeschrankung, Relativierung) of <1> is the unabb~eviated version of <1>, as e.g. (ii), where sort symbols are used as unary predicate symbols to express the sort of a variable symbol. Now the relation between the RP- and the ERP-calculus can be expressed by the following diagram:

Here sE denotes the extension of a set S of well sorted clauses by all functionally­ reflexive axioms [WR73] and o denotes the empty clause. l""f denotes a deduction in the ERP-calculus and 1- stands for a deduction in the RP-calculus. We assume that the set of sort axioms A E is in clausal form and we A let S denote the set of all relativizations of the well sorted clauses in S.

In the diagram, (1) and (3) express the soundness and completeness of the ERP- and the RP-calculus respectively. The ~valen~ (2.1) and (2.2) are called the So~t-Theo~em (Sortensatz), (2.1) is its modeltheMetic pa~t and (2.2) its p~oo6theo~etic pa~t.

The Sort-Theorem establishes the connection between both calculi and also shows the advantages we have in using a many-sorted calculus: We obtain a !.>ho~te~ refutationof a ~malle~ set of 1.>ho~te~ clauses, when proving SE l""f o instead of ~E U A E 1- o. The reason is that deductions about sort-relat­ ionships, which are performed explicitly in the one-sorted calculus, are built into the in6e~ence mechani~m in the many-sorted calculus.

In this paper, we shall show the soundness and completeness of the ERP-calculus (1), as well as the modeltheoretic part of the Sort-Theorem (2.1), i.e. we show that the above diagram is commutative. We shall also consider te~m ~ew~iting unde~ ~o~t~ because important aspects of paramodulation are related to term rewriting.

We shall demonstrate that the ERP-calculus is only complete if it contains a special inference rule, the so-called weaRening ~ule. This rule is specific to a many-sorted calculus, because it cannot be applied if only one sort is given, and hence in our formulation the RP-calculus is but a special case of the ERP-calculus. We also present special results about uni6ication unde~~o~t~ which are necessitated by the weakening rule.

The p~actical application of the ERP-calculus in Automated Theorem Proving leads to a d~a~tic ~eduction o6 the 1.>ea~ch ~pace as compared to the RP-calculus. This has been demonstrated by an implementation of the ERP-calculus in an existing proof procedure

[BES81 ,Ohl82].

This paper is a shortened version of the technical report [Wal82a] to which the reader is referred for the omited proofs.

It is assumed that the reader is familiar with the basic terminology of resolution and paramodulation based theorem proving (e.g. [Lov78]).

The. RP- Calc.ulu-6 Let T denote the set of all well formed te~m-6 over the alphabet of va~iable. -6ymbol-6 Q, the alphabet of c.on-6tant -6ymbol-6 t and the alphabet of 6unc.tion -6ymbol6 F. AT (LIT) is the set of all well formed atom-6 (lite.~al-6) over Q, (, F and the alphabet of p~e.dic.ate. 6ymbol-6 P.

For each literal L, ILl is the atom of L and Lc denotes L's c.omple.me.nt which is obtained from L by applying (or omiting) the negation sign not. The c.lau-6e. language. £is the set of all clauses. o is the empty c.lau-6 e.

For a set D of terms, literals or clauses, va~-6(D) is defined as the set of all variable symbols in D. The subscript g~ abbreviates g~ound, e.g. Tgr is the set of all g~ound te.~m-6.

When concerned with equality reasoning, we use E as the syntactic equality -6ign and assume E E P. SE denotes the e.xte.n-6ion of the clause set S by all functionally-reflexive axioms [WR73]. The set of all equality atom-6 ATE is defined as ATE= {E(q r) lq,rE T}.

SUB is the set of all -6ub6titution-6 and c denotes the identity -6ub-6titution.The domain of a substitution a, denoted DOM(a), is the set of all variable symbols x with ax * x. The c.odomain of a , denoted COD (a) , is defined as a(DOM(a)). We say that two substitutions 6 and A ag~e.e. on a subset V of Q, denoted e = A[V],iff ex= AX for each x EV.

A (g~ound) te.~m ~e.w~iting -6y-6te.m is a set of

directed equations R = { E (q. r.) E ATE 1 i E J} l. l. gr where J c N . We define ·R by q =>Rr iff E (q r) E R and we use -+R to denote the ~e.duc.tion ~elation associated with R(cf. [H080]). ~R is the t~an-6itive. c.lo6u~e. of -+R.

We shall also manipulate g~ound lite.~al-6 by a term rewriting system and extend ~R in the obvious way. For a set I of literals, the te.Jtm ~e.w~itin.g -6y-6te.m R(I) c.ontai¥t e.d -<.n I is defined as R (I) = In ATE . gr

Given a variable disjoint set S of clauses and a clause C, S 1- C denotes the existence of a deduction of C from S, using the in­ ference rules of factorization, resolution and paramodulation. S IR C is a deduction without paramodulation and S IP C is a deduction without resolution. S denotes gr the set of all g~ound in-6tanc.e.-6 of the clauses in s.

A (possibly infinite) subset I of LIT is gr called an inte.~p~ e.tation iff for each LEI, Lc It I. I is E-c.lo-6e.d iff for each LEI and each KELITgr' KEI whenever L ~R(I) K. Iis an E-inte.Jtp~e.tation iff I is E-closed and E (t t) E I for each t E T .

gr

The. r RP-Calc.ulu-6 Let $ be a set of -6o~t 6ymbol-6 ordered by the 6ub6o~t o~de.~ $ 5 ,i.e. a partial order which is reflexive, anti­ symmetric and transitive. We use s 1 « s s 2 as an abbreviation for: s 1 < 5 s 2 such that there is nos with s 1 < 5 s < 5 s 2 . Variable, constant and function symbols are associated with a certain sort symbol, called the ~ange.-6o~tof the respective symbol. The -6o~t [t] of a term t is the rangesort of the outermost function, constant or variable symbol of t.

All argument positions of a function or pre­ dicate symbol are associated with a certain sort symbol called the domain-6o~t. In the construction of the set Tr of all r-te~m-6 (or well -6o~te.d te.~m-6) and of the set ATE (LITE) of all r-atom-6 (r-lite.~al-6) of the ERP-calculus, only those terms may fill an argument position of a function or predicate symbol, whose sorts are subsorts of the domainsort given for the respective argu­ ment position. For equality atoms we assert E ( t1 t2) EAT l: iff t1 I t2 E T l: .

A l:-~£au6e is a finite subset of LITE. The many- 6 o~t ed tanguag e Cl: is the set of all l: ­ clauses. T,. ,. gr denotes the set of all variable free E-terms. AT , Egr defined in a similar LITl: gr and Cl: gr are way.

Sometimes we use sort symbols also as unary predicate symbols. Then we assume that s is the only domainsort of s E ~ and we define s s . LIT (LITE) as the set of all (l:-)llterals in the ext ended tanguag e c 5 (C~).

The set Al: of all 6o~t ax~o m6 is the smallest variable disjoint subset of C~ whichsatisfies

1. {s (c)} E Al: , if c E C has rangesort s,
2. ( 2) { not s 1 ( x 1 ) , ... , not sk ( xk ) , s ( f ( x 1 ... xk))} E Al: , if f E F has s 1 , ... ,sk as domain­ sorts and has rangesort s,and each xi E lJ has rangesort si, and
3. {not s 1 (x),s 2 (x)} EAE, if s 1 « 5 s 2 . The ~ etat~v~zat~on ~ of a l: -clause C is a clause in C~ and defined as

1\ C = {not s 1 (x 1 ), ... , no t sn (xn)} U C, where {x 1 , ... ,xn} = vars (C) and each xi has range­ sort si.

For a set S of 1\ { CEC~ICES}. 1\ l:-clauses, S abbreviates

A l:- 6ub6t~tut~on o is a substitution satis­ fying

• (*) oxETl: and [ox] s 5 [x], for eachxEIJ.

It can be shown that (*) is equivalent to o (T l: ) c T l:. SUBE denotes the set of all l:­ substitutions. A l:-~enam~ng 6ub6t~tut~on v for a set D of variables, literals or clauses is a renaming substitution for D such that [ vx] = [x] for each x E IJ.

For a l:-clause C and a E-substitution o, oC is called a E-g~ound ~n6tan~e of c, if oC E Cl:gr A set D of E-terms or E-atoms is E -un~ 6 ~abt e iff D is unifiable with a l:-sub­

stitution o. Then o is a E-un~6~e~ of D. o is

• a l: -most general unifier (E-mgu) of D iff o is mgu of D and o E SUBE .
• A l: -substitution ~ is a wea~en~ng 6ub¢~on for a set Vc lJ iff ~ satisfies
• COD(~ ) c IJ\V
• ~ I V is injective
• [~x] < [x], if x E DOM( ~ )
• s

For each V c IJ, WSUB(V) denotes the set of all weakening substitutions for V. Obviously e: E WSUB (V) and WSUB (V) c SUBE .

For a (ground) term rewriting system R we define the E-~edu~t~on ~etat~on -+l:R associated + with R by -+l:R = -+R n (Tl:gr X Tl:gr). ---+l:R is the transitive closure of -+ l: R. R is a l: ­ max~ma£ term rewriting system iff "*R = 2..ER. Note that in general a E-maximal term re­ writing system is ~n6~n~te.

If a clause c is a resolvent, paramodulant or a factor of some E-clauses, then C is a l:-~e6o£vent, E-pa~amodutant or E-6acto~ respectively, provided the mgu used to form ion, the modut ant t~te~at [Lov78] is a l:­

C is a l:-mgu and in the case of paramodulat­ literal.

If c E Cl: and ~ E WSUB (V) for some V=>vars (C), then ~c is a wea~en ed va~~ant of C. Obvious­ ly, each l:-resolvent, E-paramodulant, l: ­ factor and each weakened variant is a l:­ clause.

Given a variable disjoint set of l:-clauses S, S IE C denotes the existence of a E-de­ duction of C from S, i.e. S 1- C and each clause in this deduction is a l: -renamed l:­ resolvent, l:-paramodulant, E-factor or weakened variant. S IER C denotes a l:-de­

duction without E -paramodulants and S ll: P C is a E-deduction without l:-resolution.

Given a set of E-clauses S, S,. denotes the ,. gr set of all l:-ground instances of the Eclauses in S. An interpretation I l:-6~6~U a E- dau6e C iff I satisfies each E-ground instance oC of C, i.e. oC n I * ~. I E6at~6 6~e6 a 6 et o 6 E- ctau6 e¢ S iff I E­ satisfies each clause in S. In this case, I is

• and

a E-model of S and S is E-.6at..L.66..Lable. If in addition I is an E-interpretation, then I EE-.6at..i..66..i.e.6 S, I is a EE-mod el of S and s

is EE-.6at..L.66..Lable.

Throughout this paper <$, s 5 > is a partially ordered set of sort symbols and S stands for any variable disjoint set of E-clauses.

3. The Weaken..Lng Rule

The following examples should provide some motivation for our work illustrating the notions introduced so far and also demon­ strate that the ERP-calculus is incomplete without the weakening rule. Essentially there are two reasons for this incomplete­ ness:

1. the Unification Theorem [Rob65] does not hold in the ERP-calculus,
2. pararnodulation is incomplete in the ERP­ calculus (without the weakening rule).

Example 4.1 Let $ = {A,B,C,D} with D « 5 B « s A and D « s C « s A and l e t P E P , d E C and {u,v,w} c ~ such that A is the only domainsort of P, D is the rangesort of d and w, B is the rangesort of u and C is the rangesort of v. Now consider the set of E­ clauses S = {{ P(u)}, {not P(v) }} . Sis E-un­ satisfiable, because s" = {{P(d)},{notP(d)}} "gr is unsatisfiable. But neither cr = {u+v} nor T = {v+u} are /:-substitutions, i.e. no E-re­ solvent can be derived from the two clauses in S. But with the weakening rule, we find a /:-refutation of S:

• (C1) Vu. {P(u)} , given
• (C2) Vv. {not P(v)} , given
• (W1) Vw. {P(w)}

W1 is a weakened variant ~C1 of C1, where ~ = {u+w}, and R2 is a E-resolvent of C2 and W1, because e = {v+w} is a E-mgu of {P(v), P (w)}.

Note that we propose the weakening rule as an additional inference rule only in order

to isolate the crucial point and to obtain completeness results. In a p~oo6 p~oQedu~e this rule is realized by a modification of the un..L6..i.Qa;t..i_on algo~..Lthm, i.e. in our system [BES81,0hl82] the empty clause is derived from C1 and C2 by a single resolution step using the substitution eo~ { u+w ,v+w}.

However this modification of the unification algorithm only covers applications of _the weakening rule as in the above example. Un­ fortunately there are cases which cannot be solved using the modified unification algorithm:

Example 4.2 Let$= {A,B} with B « 5 A and let PEP, {b 1 ,b 2 } cC and { x,y,z } c~ such that B is the only domainsort of P, A is the rangesort of x and y,and B is the rangesort of b 1 ,b 2 and z. S = {{ P(b 1 )}, {E(x y)}, {not P(b 2 J}} is a EE-unsatisfiable set of E-clauses because SEgr = {{P(b 1 Jl,{E(b 1 b 2 ll, ... , {not P(b 2 )}} is E-unsatisfiable. We can derive four pararnodulants from S, namely {P(x) } ,{P(y)}, {not P(x)} and {not P(y)} none of which is a E-clause, i. e . not a E-para­ modulant. But with the weakening rule we

find a /: -refutation of S:

W4 is a weakened variant ~C2 of C2, where ~ = {y+z} , PSis a E-paramodulant of C1 and W4 and R6 is a /: -resolvent of PS and C3.

1. Te~m R ew~..Lt..Lng unde~ So~t.6

We present a result for (ground) term re­ writing under sorts, which is essential for

the completeness of the ERP-calculus in the

ground case:

The l: -Rewrite Theorem obviously also holds for R-rewrites of ground literals.

1. �~ou~d Complete~e~~ o6 the ERP-Calculuc At the E-ground level there is no difference between resolution and E-resolution. Hence the main difficulty is in showing the result for pararnodulation, i.e. to prove a result which links E-deductions IEP to deductions IP from a set of E-ground clauses. To this e ffect we need the following definition:

Ve6..i.~it..i.o~ 5.1 Par(S) = {C E C ISE 1-p C} gr Egr ParE (S) RPAR(S) E = {C E (EgriSEgr IEP C} , and E = {CEI:grlsl:gr 1p C, such that no clause in lp is obtained by para­ modulating into a positive equality literal} .

As a prerequisite for the proof of the Ground Completeness Theorem we show that if ParE (S) is satisfiable, then RPar(S) is satisfiable. As a first result we obtain:

Lemma 5.1 If ParE (S) is satisfiable, then it has a model M cLIT,. , such that R(M 0 ) o .. gr is a E-maximal term rewriting system.

The above model M 0 is E-closed, relative to + ~l: R(Mo), i.e. we can prove the following:

Lemma 5. 2 If L EM and K E LIT such that + o gr L --> l: R (M ) K, then · K E M 0 ·

0

Now let the ~ew~..tte-clo~u~e M* of M be M 0 0 0 extended by all ground literals which are obtained by rewriting the ground literals in M 0 (which are different from equality atoms) using the reduction relation ~R(M )"

Using the above lemmata, we can prove 0 that the rewrite-closure is always an inter­ pretation :

Lemma 5.3 If Parl:(S) is satisfiable, then it has a model M c LIT ,. , such that M* is o .. gr o an interpretation.

If we assume by contradiction that M~ con­ tains a pair of ground literals Q and Qc, then we can find a pair of l:-groundliterals L and K in M such that L + Kc. But o ~R(M 0 ) Kc E LIT,. si nee K E LIT,. , hence by the .. gr .. gr

. + c E-Rewrlte Theorem L-l: R(M )K because R(M 0 ) is E-maximal by Lemma 5.1~ Using Lemma 5.2 we obtain Kc EM , i.e. {K,Kc} c M contraa o dieting that M 0 is an interpretation.

It is easily proved by induction on the length n of a deduction S~gr IP C, that M~ satisfies each clause C E RPar(S), i.e. we can prove the following:

Lemma 5.4 If ParE(S) is satisfiable, then it has a model M 0 such that M~ is a model of RPar(S).

and we finally obtain the

�~ou~d Complet e ~e¢¢ Theo~em 6o~ l:RP If SEgr is E-unsatisfiable, then s~gr IE D,

• If S,. is E-unsatisfiable, then Par(S) is .. gr E-unsatisfiable because SEgr c Par(S). By Theorem 1 from [WR73] we infer that Par(S) is unsatisfiable, hence RPar(S) is unsatis­ fiable [Lov78] and by contraposition of Lemma 5.4 ParE (S) is unsatisfiable. But then SE 1- o by the completeness of resolution Egr E [Rob65], because there is no difference between resolution and E-resolution in the E-ground case and each clause in ParE(S) can be obtained by a E-deduction IEP from SE l:gr
• U~..i.6..i.cat..i.o~ u~de~ So~t¢

Since the Unification Theorem does not hold for unification under sorts, we must content ourselves with a weaker result. For unification under sorts, the notion of E­ compat..i.b..i.l..i.ty plays a central role:

Ve6..i.~..i.t..i.o~ 6.1 Let DcTE be unifiable. Dis E-compat..i.ble iff [ x ] ,; [y] or [x] ;:, [y] for $ $ all x ,y E vars (D) with -rx = -ry, where -r is an mgu of D.

We can show that each E-unifiable set of E­ compatible E-terrns possesses a E-mgu :

Lemma 6.1 Let DcTE beE-unifiable. If D is E-compatible, then there exists a E-mgu of D.

This is proved by showing that among the mgu's of D (which are equivalent up to variable renamings) , we can always find a E-mgu of D.

For arbitrary sets of E-unifiable E-terms, we enforce the existence of a E-mgu using a weakening substitution:

E- Un -<.6-<.c. a:t .<.on Th e.o!te.m Given DcTE, VclJ and 0 E SUBE with vars (D) c V and e unifies D, there exist 11 , o , A E SUBE such that

• ( 1) 11 E WSUB (V)
• o is an mgu of 11D , and
• 8 = Aooo11 [V]

It is easily proved, that for each E-uni­ fiable set of E-terms D, there exists some 11 E WSUB (V) such that 11D is sti 11 E-unifiable and in addition is E-compatible . By Lemma 6.1 there exists a E-mgu o of 11D and since o is an mgu we find some A E SUBE such that condition (3) is satisfied.

Note that the E-Unification Theorem ob­ viously also holds for E-unifiable sets of E-atoms.

1. Soundne.~~ and Compt e.te.ne.~~ o6 the. ER P­ Catc.utul.l

The soundness of the ERP-calculus is an immediate consequence of the following:

Soundne.l.l~ Le.mma 6o!t ERP Let M be an E­ interpretation and C E CE. If M E-satisfies S and S IE C, then M E-satisfies C.

The completeness theorem is shown as usual for the one-sorted calculus: We prove the Lifting Lemmata for E-Resolution and for E­ Paramodulation in order to justify the Lifting Theorem for E-Deductions.

Le.mma 7.1 (Lifting Lemma for E-Resolution) Given A, DECE, LAEA, L 8 EB and 0 ESUBE such that A and B share no variable symbols, LA and L 8 are complementary and 0 unifies { ILAI, IL 8 1}, there exist a E-factor A* of a weakened variant of A, a E-factor B* of a weakened variant of B, a pair of ca:nplarentary literals LA E A* and L~ E B*, weakened variants pA* and pB* and some A , o E SUBE such that The pr=f is similar to the proof of the Lifting Lemma in the RP-calculus. The existence of the various weakened variants is guaran­ teed by the E-Unification Theorem.

With an analogous Li6ting Le.mma 6o!t E-Pa!ta­ modutat.<.on, we can prove the Li6ting The.o!t e.m 6o!t E-Ve.duc.t.<.onl.l as in the one-sorted calculus and using the Ground completeness Theorem for ERP, we finally obtain the

Compte.te.ne.l.ll.l Th e.o!te.m 6o!t ER P If S is EE­ unsatisfiable, then SE IE o.

1. Th e. So!tt-The.o!te.m

In this section the Sort-Theorem for the ERP-calculus is stated. We need the follo­ wing two lemmata:

Le.mma 8.1 If M is an E-model of (~ U AE)gr' then M E-satisfies S ~ "gr

This lemma is used to prove one direction of the equivalence stated in the Sort-Theorem. The reverse direction is obtained with more difficulty:

Le.mma 8.2 If S~ is E-satisfiable, "gr then (g U AE) is E-satisfiable. L-------~g~r~-----------------A----~---------J

We obtain an E-model M* of (S U AE) gr from an E-model M c LIT of S~ by setting gr ugr M*=(M U rMll U (M U rMllc, where the Re.!tne.t rMl of M is the set of all literals of form s (t) , t E T and s E S, for which there exists gr a q ET~ with [q) :.; sand E(q t) EM, and "gr S the ~-c.ompte.me.nt (M U rMllc of (M U rMll is the set of all literals of the form not s (t) , t E T and s E ~I with s (t) Et (M u rMl) . It gr can be proved that M* is an E-interpretation (whenever M is an E-interpretation with M n LIT~ ¢) , and that M* satisfies A gr (S U AE)gr

The connection between the RP- and the ERP­ calculus is now established by the SoJtt-The.oJte.m 6oft the. l: RP-Ca£.c.u£. uJ.> s is l:E­ unsatisfiable iff (~ U Al:) is E-unsatis­ fiable.

S is l:E-unsatisfiable iff S~ is E-unsatis­ ,. gr fiable, which is equivalent to the E-unsatisfiability of (~ U Al:) by Lenmata 10.1 and 10.2. But (~ U Al:) o/ A ~ is E-unsatisfiable iff (S U Al:) is E-unsatisfiable by the Herbrand Theoren and by the Canpactness Theoren.

1. An Automated Th e.oJte.m P!tove.Jt no!t the. l:RP­ Ca.f.c.u£.u~.>

In [Wal82a] a survey is presented of how an automated theorem prover based on the RP­ calculus can be modified to obtain an auto­ mated theorem prover for the l: RP-calculus. The necessary modifications concern the in­ >Jut-£.anguag e. compiler, the 1.> lw £.e.mization routine, the uni~ic.ation algorithm, and the c.omputation of factors, resolvents and para­ modulants. The Markgraf Karl Refutation Procedure [BES81 ,Ohl82] was adapted to the l:RP-calculus according to the modifications stated above. BelON a proof protocol of the new systen is presented, proving a many-sorted version of the well-knONn monl<e.y-banana-p!tob£.e.m [ Lov7 8] :

NARKGRAF KARL RrFUTATION PROCEDURE, UNI KARLS RUHE , VERSION 12-0CT-8 2 DA1 E: 2-NOV-~2 16:46:27

·······································································

AXI GAS GIVEN 10 TH~ THEOREM PROVER : SORT ANIMAL ,TALL:IN. ROOM TYPE BANANA,FLOOR:I N.ROOM TYl'E CHAIR:'I'ALL 'I"Y ~E 1'YPt: '.iYI:'E TYPE Tl:PE 'lYt>E TYt'E l\Xr-11 AX~i 2 AXM3 AXM4 AXMS AXM6 AXJ'17 riOt<KEY: ANIMAL CAN. REACrl(ANIMAL I N.ROOM) CLOSE.'I'O(I~.ROOM IN.ROOM) ON(IN.ROOM IN.ROOM) UNDER(I N.ROOM I N.ROOM) CAN.MOVE.NEAR(ANIMAL I N.ROOM I N. ROOM ) CAN.CLIMB(ANIMAL TALL) ALL X:ANIMAL Y:I N.ROOM NOT CLOSE.TO(X Y) OR CAN.REACH(X Y) ALL X:ANIMAL Y:TALL NOT ON(X Y) OR NOT UNDER(Y BANANA) OR CLOSE.TO(X BANANA) ALL X:ANIMAL Y:IN.ROOM Z:IN.ROOM NOT CAN.MOVE.NEAR(X Y Z) OR CLOSE.TO(Z FLOOR) OR UNDER(Y Z) ALL X:ANIMAL Y:TALL NOT CAN.CLIMB(X Y) OR ON(X Y) CAN.MOVE.NEAR(MONKEY CHAIR BANANA) NOT CLOSE.TO(BANANA FLOOR) CAN.CLIMB(MONKEY CHAIR) THEOREM GIVEN TO THE THEOREM PROVER: AXM2 RE.Sl AXMl AXM6 THM8 RESS RES6 THMB : NOT CAN.REACH(MONKEY BANANA) + AXM3 --> + AXMS --> + RES2 --> + RES3 --> + RES4 --> + AXM4 --> + AXM7 --> RESl RES2 RES3 RES4 RESS RES6 RES? ALL X:ANIMAL Y:TALL Z:ANIMAL CLOSE.TO(X BANANA) OR NOT ON(X Y) OR CLOSE.TO(BANANA FLOOR) OR NOT CAN.MOVE.NEAR(Z Y BANANA) ALL X:ANIMAL CLOSE.TO(BANANA FLOOR) OR NOT ON(X CHAIR) OR CLOSE.TO(X BANANA) ALL X:ANIMAL CAN.REACH(X BANANA) OR NOT ON(X CHAIR) OR CLOSE.TO(BANANA FLOOR) ALL X:ANIMAL NOT ON(X CHAIR) OR CAN.REACH(X BANANA) NOT ON(MONKEY CHAIR) NOT CAN.CLIMB(MONKEY CHAIR) EMPTY THE FOLLOWING CLAUSES WERE USED IN THE PROOF! AXM7 AXM4 AXMS AXM3 AXM2 RESl RES2 AXMl RES3 AXM6 RES4 THM8 RESS RES6 RES7 ·

THE THEOREM IS PROVED. END OF PROOF 2-NOV-82 16:47:22.

In our system, we use the expressions (cf. [Wal82b])

SORT s 1 , ... ,sn:s to denote si « 5 s

TYPE c 1 , ··· ,cn:s to denote that ci E (:

has rangesort s

TYPE P (s 1 ··· sn)

to denote that PEP

has the domainsorts s 1 , ·.. ,sn , and

ALL x:s to denote the universal

quantification of a variable symbol x with rangesort s.

The first column lists the statistical values for the proof using the many-sorted calculus,the second column lists the values for the one-sorted calculus and the third column shows the ratio between the values of both example runs.

In the proof statistics, the value for 'number of links generated' corresponds to the size of the search space,the value for 'number of steps executed' is a measure of the expense of the actual search and 'level of proof' represents the search depth.

The comparison between the statistical values of both protocols immediately reveals the advantages of using an automated theorem prover based on the l:RP-calculus. The values are typical for all examples(and of course for more complex ones) that have been proved by this system.

A c.lmow.l'. e.d g e.m e. n.-t-6

I would like to thank my colleagues K.-H. B.l'.af.Jiu-6, N. Ei.6in.ge.~, H.J. gh.e.bac.h and W. S-te.phan for their support during the preparation of this work, and also A. He.~o.l'.d for the useful discussions on Unification Theory. J. Si e. Rman.n. read an earlier draft of this paper; his helpful criticism and support greatly contributed to the present form of this paper.

The system also solved the monkey-banana­ problem, using the one-sorted axiomatizat­ ion from [Lov78]. The following diagram shows the proof statistics of both examples runs: