Implementing Restart Model Elimination and Theory Model Elimination on top of SETHEO

Implementing Restart Model Elimination and Theory Model Elimination on top of SETHEOPeter BaumgartnerUniversity of KoblenzRheinau156075KoblenzGermanypeter@informatik.uni-koblenz.deJohann SchumannInstitut f¨u r InformatikTechnische Universit¨a t M¨u nchenGermany80290M¨u nchenschumann@informatik.tu-muenchen.de AbstractThis paper presents an implementation for the efficient execution of Theory Model Elimination(TME),TME by Linearizing Completion,and Restart Model Elimination(RME)on top of the automated theorem prover SETHEO.These calculi allow for theoryreasoning using a Model Elimination based theorem prover.They are described indetail and their major properties are shown.Then,a detailed description how TME byLinearizing Completion and RME can be implemented on top of SETHEO’s AbstractMachine(S A M)is given.Due to theflexibility of the Abstract Machine and its inputlanguage LOP,only simple transformations of the input formula are sufficient to obtainan efficient implementation.Only for RME,one machine-instruction of the S A M had tobe modified slightly.We present results of experiments comparing plain SETHEO withan implementation of TME with PTTP(PROTEIN)and the SETHEO implementationpresented here.1IntroductionThe model elimination calculus(ME calculus)has been developed already in the early days of automated theorem proving[Loveland,1968].It is a goal-oriented,linear and refutationally complete calculus forfirst order clause logic.Model elimination is the base of numerous proof procedures forfirst order deduction.There are high speed theorem provers,like METEOR ([Astrachan and Stickel,1992]or SETHEO([Letz et al.,1992,Letz et al.,1994])and there is a whole class of provers,namely Prolog technology theorem proving(PTTP)as introduced in [Stickel,1988,Stickel,1989],which rely on model elimination.This paper deals with several variants of model elimination with an emphasis on the implementational issue.These variants are called restart model elimination[Baumgartner1and Furbach,1994a]and theory model elimination[Baumgartner,1992,Baumgartner,1994]. They will be reviewed in the respective sections below.For a more detailed description the reader is referred to the cited literature.In brief,restart model elimination is a variant which was motivated by taking a logic programming view at theorem proving.In logic programming one typically reads a clause operationally as a“contrapositive”which means,roughly,“in order to prove it suffices to prove and”.However,in (ordinary)model elimination in the presence of non-definite clauses(i.e.,clauses with more than one positive literal)this natural reading has to be given up.For completeness reasons it is required to add the contrapositivesIn other words,the“body”literals and have to be considered as entry points for the proof search,too.Why should we bother with these contrapositives?Suppose,for example we are given an input clause1which can be used within a formalization of propositional calculus.A possible contrapositive isThe procedural reading of this contrapositive is somewhat strange and leads to an unnecessary blowing-up of the search space;in order to prove one has to prove–a goal which is totally unrelated to by introducing a new variable.Now,the question arises whether model elimination can be modified in such a way that the above“natural”contrapositives suffice.Indeed,this is achieved in restart model elimination (there are also several other calculi achieving this,e.g.Loveland’s NearHorn-Prolog[Loveland, 1987],Gabbay’s N-Prolog[Gabbay,1985]and Plaisted’s problem reduction formats[Plaisted, 1988]).In restart model elimination,for non-definite clauses,likeonly the following contrapositives have to be considered:It is even possible to restrict to one of those(cf.the selection function below).Of course there is a price to pay.In restart model elimination an additional inference ruleis needed,the restart rule,which allows to begin a completely new proof once a negative bodyliteral,such as or is encountered.As mentioned above,restart model elimination is motivated by logic programming.Be-sides that,we think that restart model elimination is also useful in an automated theoremproving context:in proving theorems such as“if0then20”a human typically uses case analysis according to the axiom000.This seems a verynatural way of proving the theorem and leads to a well-understandable proof.Restart modelelimination carries out precisely such a proof by case analysis.Now let us turn to the other variant,theory model elimination.Theory reasoning wasintroduced by M.Stickel within the general,non-linear resolution calculus[Stickel,1985];formodel elimination it is defined and investigated in[Baumgartner,1992,Baumgartner,1994].Theory reasoning means to relieve a calculus from explicit reasoning in some domain(e.g.,equality,partial orders,taxonomic reasoning)by taking apart the domain knowledgeand treating it by special inference rules.In an implementation,this results in a universal“foreground”reasoner that calls a specialized“background”reasoner for theory reasoning.The advantages of theory reasoning,when compared with the naive method of supplying thetheories’axioms as clauses,are the following:for thefirst,the theory inference system maybe specially tailored for the theory to be reasoned with;thus higher efficiency can be achievedby a clever reasoner that takes advantage of the theories’properties.For the second,a lotof computation that is not relevant for the overall proof plan is hidden in the background.Thus proofs become shorter and are more compact,leading to better readability(although werecognize that this is a matter of taste).More technically,in theory reasoning the idea offinding complementary literals is gener-alized to a semantic level.For instance,in the theory of strict orderings,the literals, and may be detected to be inconsistent by the background reasoner.The general idea is to do the search for complementary literals on this semantical level at every place where syntactical reasoning is used in the non-theory version of the calculus.The question arises how to obtain for a given theory a background calculus.To this end,one of the authors has designed a compilation technique which allows to transform a Horntheory into inference rules which are suitable to be used in conjunction with model elimination.This method,called linearizing completion[Baumgartner,1995]is used throughout all ourexperiments.Fortunately,theory reasoning can be applied to ordinary model elimination,as well asrestart model elimination in a complete way.Together with various sub-variants of restartmodel elimination we have now a considerable spectrum of different calculi for differentneeds of automated reasoning at hand.It is the purpose of this paper to evaluate some of thesecombinations by using the Setheo theorem prover.The rest of this paper is structured as follows:after concluding this introduction withsome preliminaries(basic definitions)we will briefly review the model elimination calculus(Section2).Then we generalize it towards theory model elimination in Section3.Section4describes another calculus variant,restart model elimination.Implementation on SETHEO isdiscussed in Section5.Finally,Section6reports on experimental results.31.1PreliminariesA clause is a multiset of literals,written as the disjunction1.As usual,clauses areconsidered implicitly as being universally quantified,and a clause set is considered logicallyas a conjunction of clauses.Instead of the chains of the original model elimination calculuswe follow[Baumgartner and Furbach,1993]and work in a branch-set setting.A branch is afinite sequence of literals,written by juxtaposing its constituents12.A branch set isafinite multiset of branches.Concerning interpretations we restrict ourselves to Herbrand-Interpretations over a(mosttimes implicitly)givenfinite signatureΣ.Furthermore we supposeΣto contain the0-arypredicate symbol which is to be interpreted by in every interpretation.We assume atheory to be given by a satisfiable set of universally quantified formulas,e.g.as a clause set(because a Herbrand-theorem holds).In the sequel always denotes such a theory.As anexample one might think of the theory of equality,given by the usual axioms.A Herbrand -interpretation for a formula is a Herbrand-interpretation over the joint signatures of and that satisfies,i.e..We write to indicate that is a-interpretation and satisfies(i.e.is a-model for).Furthermore,is called-valid,F,iffevery-interpretation satisfies,and is-(un-)satisfiable iff some(none)-interpretationsatisfies.As a consequence of these definition it holds iff is-unsatisfiable iff is unsatisfiable.2Review of Model EliminationWe will briefly and rather informally review our format of model elimination.It differs from the original one presented by[Loveland,1968];the format we use is described in[Letz et al., 1992]as the base for the prover SETHEO.In[Baumgartner and Furbach,1993]this calculus is discussed in detail and compared to various other calculi.This model elimination manipulates trees by extension-and reduction-steps.As an example consider the clause setA model-elimination refutation is depicted in Figure1.It is obtained by successive fanning with clauses from the input set(extension steps.Additionally,it is required that every inner node(except the root)is complementary to one of its sons.An arc indicates a reduction step, i.e.the closing of a branch due to a path literal complementary to the leaf literal.We will nor present the inference rules formally,because this is done in a more general form in the following section.3Theory Model EliminationIn this section we will review the extension of model elimination towards theory reasoning.A more thorough treatment can be found in[Baumgartner,1994].Theory reasoning comes in two variants[Stickel,1985]:total and partial theory reasoning. Total theory reasoning directly lifts the idea offinding syntactical complementary literals4******Figure 1:A Model Elimination Refutationin inferences (e.g.,resolution)to a semantic level.In partial theory reasoning semantical complementary sets are computed stepwise by means of intermediate goals (called “residues”).The partial variant is of particular interest for us because we have a technique to automatically construct background reasoners for partial theory model elimination [Baumgartner,1995].This technique,called linearizing completion is briefly described below in Section 3.1.Definition 3.1(Theory model elimination (TME))The inference rule theory extension step which transforms a branch set and some clauses in a new branch set is defined as follows:K 1K m L 1R 1L n R n2Residues can be generalized to clauses as in [Stickel,1985],if it is of interest.5K1K m F1result for thefirst-order case with variables would be technically much more complicated (cf.[Lloyd,1987]).Completeness is stated for the ground case only.Although not quite trivial,lifting to the first order case can be carried out by generalizing standard techniques(see e.g.[Chang and Lee,1973,Lloyd,1987]).Theorem3.5(Ground Completeness of Regular Total TME)Let be a theory,c be a computation rule and let M be a-unsatisfiable ground clause set.Let C M be such that C is contained in some minimal-unsatisfiable subset of M.Then there exists a regular total TME refutation of M wrt.c with query C.For the ground proof the excess literal parameter technique can be used in a similar way as it is done for the non-theory version in[Baumgartner and Furbach,1994a].Regularity is shown by restricting for every branch to be closed the available input clause set to those clauses that are free of literals occurring in that branch.An important class of theories are definite theories,i.e.,theories that are axiomatized by a set of definite clauses3.For such theories wefind a special structure of implications: Proposition3.6For every definite theory and for every-valid implication L1L n L n1it holds that either(1)all literals L1L n and the conclusion L n1are positive, or(2)one single literal L i(1i n)is negative and L n1is either negative or F.This special structure of implications can immediately be imposed on the corresponding implications in the definition of extension steps above.If additionally the input clause set is “Horn”,then the ancestor literals of leafs need not to be stored and all extending literals are positive.This result generalizes a well-known property of ordinary model elimination,which states that no reduction steps are required(even possible)in the Horn case.3.1Partial Theory Model Elimination by Linearizing CompletionLet usfirst give some motivation for the linearizing completion technique from the viewpoint of partial theory model elimination.Recall from the definition of theory model elimination(Def.3.1,in particular condition3) that we distinguish between total and partial theory model elimination,where the latter differs from the former only by the possibility to derive residues(i.e.,new subgoals)different from .In other words,in total theory model elimination the contradiction must be discovered by the background reasoner in a single step,while this need not necessarily be so in partial theory model elimination.However,it may be practically difficult or even impossible to design an appropriate background calculus for total theory reasoning.Consider e.g.the theory of equality,where the background calculus then must be capable to enumerate all solutions for a given rigid E-unification problem[Gallier et al.,1987].However the decidability of simultaneous rigid E-unification is still open.No matter how this question will eventually be answered,there are(other)undecidable theories.For undecidable theories we can expect to obtain at mostan enumeration procedure for solutions rather than an algorithm.So,the computations in the background calculus have to be interleaved with the foreground calculus.This makes it difficult to treat the background calculus as a“black box”.In order to remedy the situation,partial theory model elimination offers the framework to split the one single total extension step into a sequence of partial extension steps,followed by a concluding total step.Take the example of equality again.Then,for instance,a total step involving rigid E-unification can be replaced by a sequence of paramodulation steps which transforms an initially given equational goal into which in turn is to be closed by a trivial total step.However,as defined so far,the difficulty with the partial variant is that it adds possible inferences,but does not restrict the total inferences.Thus,partial theory model elimination can be seen only as a framework,and completeness holds vacuously.Furthermore,for efficiency reasons one would certainly not want to consider all-valid implications(Condition3in Def.3.1again)for extension steps.Take again equality:the paramodulation inference rule does not compute all equational consequences of the given key set.For example,is such a-valid implication,but paramodulation does not allow toflip the sides of an equation.This is the point where linearizing completion comes in.The purpose of linearizing completion is to minimize both the possible total and partial extension steps.This is done in a rather general way.Linearizing completion takes as input an arbitrary Horn clause set,such as for example the following set which axiomatizes a theory of strict orderings:Then this set is saturated under certain operations(roughly:binary resolution)modulo a certain notion of redundancy(see[Baumgartner,1995]for a more accurate description of the method).The result is a–possibly infinite–set of clauses.In this case,however,we are lucky and linearizing completion produces the followingfinite set::(Irref)(Asym)(Trans-1)(Trans-2)(Syn)The associated operational meaning of,for instance,the clause(Trans-1)is“from literals and infer the literal”.Consequently,we call such clauses inference rules. Under this operational viewpoint it is clear that(Trans-1)and(Trans-2)are different,although they are logically equivalent.As in theory model elimination the conclusion as in the(Irref) and(Syn)rules stands for.Now we can get back to explain the connection between linearizing completion and partial theory model elimination.The idea is to describe the set of permissible total and partial theory extension steps by such inference rules.This shall be defined more precisely:Definition3.7(Inference systems,theory extension step based on)An inference rule is an expression of the formL1L n L n19where all L i s,1i n ,are literals (called premise literals ),and L n 1is either a literal or F (called conclusion ).The declarative meaning of an inference rule is the implication L 1L n L n 1.An inference system is a set of inference rules.On modifying the definition of theory extension step (Def.3.1)we define the inference rule theory extension step based on to be defined as theory extension step ,except that condition 3is replaced by the following:3.there exists a new variantL 1L n Resof an inference rule from ,there exist indices 1j 1j k m 1and there exists a substitution which is a most general unifier for the multisets L 1L n and K j 1K j k K m .A theory model elimination derivation based onis a derivation where all extension steps arebased on .In words,in order to carry out a theory extension step according to this definition,one has to find an inference rule from whose premise literals simultaneously unify with the leaf literal and some literals from the branch to be extended.If this succeeds the instantiated conclusion of the inference rule yields the residue.In case the conclusion is we have a total step,otherwise a partial step.It should be clear that by this device the set of possible extension steps can be pruned considerably.This holds for instance when using the above inference system for strict orderings.The soundness of this calculus obviously depends on the soundness of .It holds that theory model elimination based on is sound if every inference rule in is a logical consequence (according to the declarative reading)of the underlying theory.Completeness is much harder to establish.As a sufficient condition completeness holds if is obtained by linearizing completion,as e.g.above.We will leave this presentation of linearizing completion now.Finally,it should be noted that since linearizing completion is a tedious task if done by hand we have implemented it and used it in the experiments below.In case linearizing completion results in an infinite inference system finite approximations were used.4Restart Model EliminationLet us now modify the theory model elimination calculus (Section 3),such that only a single contrapositive per clause is needed.The modifications work for both the total as well as the partial variant.Hence we will give up the distinction in this section.For the modifications we have to presuppose definite theories (see the preceeding section).Furthermore,in order to get a complete calculus,we have to assume that there exists only one10clause containing only negative literals,which furthermore does not contain variables,and this clause is to be used as query in refutations4.We note that Theorem3.5can be adapted for this new setting.Definition4.1(Restart Theory Model Elimination)First,extension steps are restricted to operate on negative leafs only.For this define a definite theory extension step in the same way as theory extension step,except that additionally K m is required to be a negative literal and allother key set literals K j1K jkL1L n are required to be positive literals.In order to deal with positive leafs K m define the inference rule restart step as follows: K1K m4Without loss of generality this can be achieved by introducing a new clause and transforming every purely negative clause1into1.5This property is needed for the completeness proof;it guarantees for lifting that the selection function will select on thefirst order level a literal whose ground instance was selected at the ground level.111ABF CADpositive literals occurring in are pairwise distinct.For example,the refutation in Figure3is blockwise regular.Fortunately it holds:Theorem4.4Strict Restart TME with selection function is complete when restricted to block-wise regular refutations.5Implementation on top of SETHEO5.1Architecture of the SystemIn this section,we describe,how partial theory model elimination by Linearizing Completion can be implemented efficiently on the automated theorem prover SETHEO.Figure4shows the components of the system and how the input formula(a set of clauses)is processed.Then,during the compilation phase,contrapositives of the form6:-1111are generated.If0,the:-is changed to?-.Such a contrapositive is used–like in PROLOG–as a possible start clause(query).For the following,a contrapositive of a clause is labeled(for an inference rule of)where is the number of the clause,and is the index of the head literal(1).A LOP formula can contain a mixture of clauses(with<-,fanned during compilation)and contrapositives(with:-or?-,not fanned)75.2Implementation of the theory extension stepIn order to implement theory model elimination by Linearizing Completion,the theory exten-sion step based on the given set of inference rules must be realised within the framework of SETHEO.For the following,we drop the condition that the premise literals of a given inference rule must simultaneously unify with the leaf literal and literals from the branch to be extended(see Definition3.7).This restriction allows for a much easier implementation on top of SETHEO,since SETHEO’s proof procedure considers exactly one branch to be extended at a time.The extension step of Definition3.7can directly be transformed into a model elimination tableau in the following way:given a branch of the tableau with a selected literal(leaf). Furthermore,we have an inference rule:11Then a theory extension step based on this inference rule can be established by a pure model elimination tableau as shown in Figure5.The inference rule(as a clause)is appended to the leaf-node of the tableau.The following conditions must hold:1.one of the literals(1)must be complementary to the selected leaf literal.Thus this branch is closed(marked by an asterisk in Figure5).2.all other literals1(except)must be solved by(a)a model eliminationreduction step into one of the literals on the path from the current leaf to the root of the tableau,or by(b)a closed tableau.Its start clause(into which a model elimination extension step is made)must be a clause of the input formula(i.e.,a clause of the form from Definition3.1).Hence,it must not be an inference rule from.Then,the residuum literal1with the substitution applied comprise the new leaf-node of the tableau.In case,1,no new leaf node is created.This means that the branch with could already be closed.Example5.1Again consider the formula and theory of Example3.2(page6).Then step2 of Fig.2is equivalent to the tableau shown in Fig.6.146In the actual LOP clauses,the negation symbol is written as.7Of course,completeness not ensured,if not all contrapositives belonging to one clause are present in the inputfile.(cf.Section4).15A literal decorated with means8that can only have connections to the head-literals of the given contrapositives.In our case,it can have a connection to all literals of our set of clauses.It is obvious that this restriction implements our condition(2b).5.3Low-level ImplementationThe current version of the language LOP,however,does not support the direct specification of sets of connections.Therefore,the selection of connections is performed on a lower level during the preprocessing and compilation phase in the module thcomp.In afirst step,we duplicate all contrapositives of,whereby all predicate symbols of the head-literals of the copy are consistently renamed into new ones(e.g.,now gets). Thus,for a clause11from we get(1): :-1111:-1111Additionally,each contrapositive of the inference rules of is processed by renaming all tail literals(1)which are decorated by Then,we obtain contrapositives of the following structure:1:-21:-111This duplication of contrapositives and renaming ensures our condition(2b),namely that an extension step from one of the tail literals(1)of an inference rule can be possibly performed into contrapositives of only.During the compilation by SETHEO, a graph of all possible connections(“weak unification graph”,[Eder,1985])is generated. In order to ensure correct evaluation of model elimination reduction steps,the renaming of predicate symbols must be undone before the actual search starts.The graph of all possible connections,however,is not changed again.Furthermore,all methods for pruning the search space which are built into SETHEO(e.g., constraints,for details see[Letz et al.,1992,Letz et al.,1994])can be directly applied.Due to SETHEO’s pure depth-first left-to-right search,the shape of the search space is somewhat different to that of the original theory model elimination.This difficulty,however,can be overcome by assigning different costs for solving the different literals of the inference rule. For SETHEO which performs a depth-first search with iterative deepening,the cost is expressed by modifying the currently available resources(number of available levels to the depth bound). For each literal of an inference rule,the following costs have been determined empirically:if is solved by a model elimination reduction step,or a unit clause from,then the cost is0.the cost for solving a literal(1)is2,andthe cost for solving1is1.In our implementation,the changes of the resources are performed by using built-in predicates(getdepth/1,setdepth/1).5.4Implementation of Restart TME on top of SETHEOThe implementation of(Strict)Restart TME based on Linearizing Completion can be separated into two steps:implementation of restart model elimination(RME)and implementation of the theory part.Since the second step is almost identical to the transformation described above, we only focus on implementing RME on top of SETHEO.As mentioned in Section4,there are 4crucial issues wrt.non-restart model elimination:1.there is only one start clause(clause with negative literals only and without variables),2.clauses are in general not fanned into contrapositives,and3.whenever a positive literal in the tail of a clause is found,a restart step must be performed.4.only blockwise regularity can be demanded.In SETHEO,issue(1)is fulfilled automatically,since a specific start clause“?-query.”is added to the formula per default.Clauses in the input formula of SETHEO are not fanned into contrapositives,if the:-syntax is used(see also Section5.2).Then,the head-literal of such a clause is the only entry-point for extension steps into that clause.Therefore,an input clause11with and being positive atoms is converted into a set of contrapositives:their heads are exactly the positive literals9.All other contrapositives, starting with the negative literals are not needed.However,to match(3),for all positive literals,occurring in the tail of such a clause,restart-steps must be performed.In out notation, we write for some.Hence,we obtain the following set of LOP-clauses: :-211:-111The restart step itself(denoted by)must be handled within the compiler and the SETHEO abstract machine S A M.The following actions must be performed during run-time to implement the restart step:1.The current literal must be placed into the path to be available for model eliminationreduction steps,and2.a“restart”must be made,i.e.,the query“query”must be called.。