Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers

Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers F.J. Mart´ın–Mateos, J.A. Alonso, M.J. Hidalgo, and J.L. Ruiz–Reina Departamento de Ciencias de la Computaci´on e Inteligencia Artificial Escuela T´ecnica Superior de Ingenier´ıa Inform´atica, Universidad de Sevilla Avda. Reina Mercedes, s/n. 41012 Sevilla, Spain http://www.cs.us.es/{˜fmartin,˜jalonso,˜mjoseh,˜jruiz} Abstract. We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that purpose, we present a framework where we define a generic transformation based SAT–prover, and we show how this generic framework can be formalized in the ACL2 logic, making a formal proof of its termination, soundness and completeness. This generic framework can be instantiated to obtain a number of verified and executable SAT–provers in ACL2, and this can be done in an automatized way. Three case studies are considered: semantic tableaux, sequent and Davis–Putnam methods. 1 Introduction ACL2 [8] is a programming language, a logic for reasoning about programs in the language, and a theorem prover supporting formal reasoning in the logic. These components make ACL2 a particularly suitable system for reasoning about decision procedures, since proving and computing tasks can be done in the same system. Efficiency is one of the design goals of the system. Usually, it is obtained by building specific procedures to solve concrete problems. On the other hand, system characteristics make possible the development of generic procedures based on logic specifications. These generic procedures can be instantiated to obtain concrete ones [9], and this instantiation can be done maintaining efficiency to some extent. In this paper, we describe an application of the ACL2 system to reason formally about a family of propositional satisfiability decision procedures. The common pattern of these procedures is that they can be described as rule based transformation systems. For that purpose, we develop a generic framework into which these SAT–provers can be placed. A generic SAT–prover is formalized in ACL2 and its main properties are proved; using functional instantiation, concrete instances of the generic framework can be defined to obtain formally verified and Common Lisp executable SAT–provers. We will also describe how this instantiation process can be automatized. Three case studies are considered: semantic tableaux, sequent calculus and the Davis–Putnam method. This work has been supported by project TIC2000-1368-C03-02 (Ministry of Science and Technology, Spain) This paper is organized as follows. In section 2 we define a generic framework in order to build a generic transformation based SAT–prover, and we sketch a proof of its termination, soundness and completeness properties. We also describe how three well–known SAT–provers methods (tableaux, sequent calculus and Davis–Putnam method) can be placed into the generic framework. In section 3 we show how this framework can be formalized in ACL2 and how its main properties can be established. In section 4 we describe how these generic definitions and theorems can be instantiated in an automatized way, to obtain verified and executable Common Lisp definitions of tableaux based, sequent based and Davis– Putnam SAT–provers. Finally, in section 5 we draw some conclusions and discuss future work. 2 A Generic Framework to Develop Propositional SAT–Provers Analyzing some well–known methods of proving propositional satisfiability (such as sequents, tableaux or Davis–Putnam), we can observe a common behavior. They do not work directly on formulas but on objects built from formulas. The objects are repeatedly modified using expansion rules, reducing their complexity in such a way that their meaning is preserved. Eventually, from some kind of simple objects, a distinguished valuation proving satisfiability of the original formula can be obtained. If no such object is found, then unsatisfiability of the original formula is proved. We can see this behavior in the semantic tableaux method with an example (figure 1–left). From the formula (p→q)∧pa tree with a single node is built. In a first step the formula is expanded obtaining one extension with two formulas p→qand p. In a second step the formula p→qis expanded obtaining two extensions, the first with the formula ¬pand the second with the formula q. The left branch becomes closed (with complementary literals) and the right one provides a model σ. Thus, the tableaux method can be seen as the application of a set of expansion rules acting on branches of trees (the objects) until a branch without complementary literals is obtained. For this branch, a distinguished valuation (making that branch true) is easily obtained. Otherwise, all branches are closed and unsatisfiability is proved. In figure 1–right we can see how the sequent method behaves in a similar way, where objects are now sequents. So our goal in this section is to describe a generic framework where these methods can be placed. First we introduce some notation. We consider an infinite set of symbols Σand a set of truth values, B={t,f}, where tdenotes true and fdenotes false.P(Σ) denotes the set of propositional formulas on Σ(the truth values are not considered as formulas), where the basic connectives are ¬,∧,∨, →and ↔.Fdenotes the complementary of a formula F. A literal is a formula por ¬p, where p∈Σ. A clause is a finite sequence of literals. A valuation is a function σ:Σ−→ B, we denote VΣthe set of all valuations defined on Σ. The valuations are extended to P(Σ) in the usual way. We denote σ|=F when σ(F)=t, and we say that σis a model of F. A valuation σis a model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p [p→q]∗ [(p→q)∧p]∗ ¬pq (p)=1 σ(q)=1 (p→q)∧p⇒ (p→q),p⇒ p⇒p Axiom q, p⇒ σ(p)=1 σ(q)=1 Fig. 1. An example of tableaux and sequents methods of a clause C, if it is a model of some literal in C. The capital Greek letters Γand ∆(possibly with subscripts) denote sequences of formulas. We will use the notation e1, ..., ekto represent a finite sequence, and O∗to denote the set of sequences of elements from the set O. We write Γ1,F,Γ 2or Γ1,F,Γ 2,to distinguish the formula Fin a sequence of formulas. Finally, Ord denotes the class of all ordinals. Definition 1. APropositional Transformation System (for short, PTS) is a triple G=O,R,V, where O,Rand Vare sets such that R⊆O×(O∗∪{t}) and V⊆O×VΣ. We will call Othe set of propositional objects (or simply objects) and Rthe set of expansion rules. An element (O, L)∈Rwill be denoted as O;GL. Note that we allow rules of the form O;G and rules of the form O;Gt. When (O,σ)∈Vwe say that σis a distinguished valuation for O, denoted as σ|=GO. Definition 2. Given a PTS G=O,R,V: 1. A computation rule is a function r:O−→O ∗∪{t}such that r⊆R. 2. A representation function is a function i:P(Σ)−→ O . 3. A measure function is a function µ:O−→Ord. 4. A model function is a function σ:Ot−→ VΣ, where Ot={O∈O:O;Gt}. Given a PTS G=O,R,V, a computation rule rand a representation function i, we define the following algorithm SATGfor proving satisfiability of a propositional formula. Algorithm 3 (SATG)The input to this algorithm is a propositional formula F and it proceeds as follows: 1. Initially the list of objects i(F)is considered. 2. Given a list of objects O1, ..., On, an element Ojis selected. (a) If r(Oj)=t, then the algorithm stops returning Oj. (b) If r(Oj)=O 1, ..., O m, then the algorithm returns to point 2 with the list O 1, ..., O m,O 1, ..., Oj−1,O j+1, ..., On. 3. If the list of objects becomes empty, the algorithm stops returning f. The intuitive idea is simple: given F, we start with the initial object i(F) and repeatedly apply the rules of Runtil tis obtained or until there are no more objects left (termination of this process will be guaranteed by a measure function µ). In the first case, from an object Ojsuch that r(Oj)=twe can obtain a distinguished valuation using a model function, which turns out to be a model of the original formula. In the second case, the original formula is unsatisfiable. Let us now establish the main properties of this generic algorithm. Definition 4. We say that SATGis complete if for all F∈P(Σ)such that ∃σ:σ|=F, then SATG(F)=f. We say that it is sound if for all F∈P(Σ) such that SATG(F)=f, then ∃σ:σ|=F. Theorem 1. Let G=O,R,V be a PTS, ra computation rule, ia representation function, µa measure function and σa model function, such that the following properties holds: P1:Oi∈r(O)=⇒µ(Oi)<µ(O) P2:F∈P(Σ)=⇒(σ|=F⇐⇒ σ|=Gi(F)) P3:O∈O∧r(O)=t=⇒(σ|=GO⇐⇒ ∃ Oi∈r(O),σ |=GOi) P4:O∈O∧r(O)=t=⇒σ(O)|=GO then the algorithm SATGterminates for any formula and is complete and sound. Furthermore, if SATG(F)=Othen σ(O)|=F. Termination Proof: To prove termination of SATGwe must prove that point 2 is a finite loop. Assume that the list of objects in point 2 is O1, ..., On, the selected element is Ojand r(Oj)=O 1, ..., O m. We consider the relation <µin Odefined as follows O1<µO2if and only if µ(O1)<µ(O2). Obviously, <µis a well founded relation on O. Then, for every k, O k<µOjby P1. Therefore, the multiset {O 1, ..., O m,O 1, ..., Oj−1,O j+1, ..., On} is smaller than {O1, ..., On}with respect to the multiset extension of <µ(which is also well-founded as proved in [5]). This proves termination of SATG. Completeness Proof: First of all note that, by P3, if the algorithm reaches point 2–(b), σis a distinguished valuation of some object in the list considered in point 2 if and only if it is a distinguished valuation of some object in the new list built in point 2–(b). If σ|=Fthen, by P2,σ|=Gi(F). Then, by the above observation, in every list considered in point 2 exists Osuch that σ|=GO. Therefore the list in point 2 cannot become empty and, as the algorithm terminates, in some step an object Osuch that r(O)=twill be considered. Then SATG(F)=O =f. Soundness Proof: If SATG(F)=Othen r(O)=tand, by P4,σ(O)|=GO. Then, by the property noted in the completeness proof, in every list considered in point 2 exists Osuch that σ(O)|=GO. Therefore, this holds for the initial list considered i(F), i.e., σ(O)|=Gi(F), and, by P2,σ(O)|=F.2 2.1 Semantic Tableaux We consider the semantic tableaux method as it is described in [6]. The tableaux expansion rules are concisely presented using the uniform notation [14]. Using this notation, non–literal formulas are classified as doubly negated, α–formulas (equivalent to the conjunction of two components α1and α2)orβ–formulas (equivalent the a disjunction of two components, β1and β2)1. We now describe the PTS T=OT,RT,VTassociated with the semantic tableaux method. In this PTS, OTis the set of tableau branches (represented as lists of formulas), VTis the set of pairs (θ,σ) such that σmakes true every formula in θ, and RTthe set of rules given by the following rule schemata: RT1:Γ1,G,Γ 2,¬G, Γ3;T RT2:Γ1,¬¬G, Γ2;TΓ1,G,Γ 2 RT3:Γ1,α,Γ 2;TΓ1,α 1,α 2,Γ 2 RT4:Γ1,β,Γ 2;TΓ1,β 1,Γ 2,Γ1,β 2,Γ 2 RT5:Γ;Ttif Γdoes not have non–literal nor complementary formulas We define the representation function iTsuch that for every F∈P(Σ), iT(F)=F. Obviously, σ|=F⇐⇒ σ|=Ti(F) (property P2). We consider any computation rule, rT, such that, for every branch θ,rT(θ) is a rule from the above table that can be applied to θ. We define the uniform measure, denoted as u, as follows: u(F)=5∗δ↔(F)+ 2∗(δ∧(F)+δ∨(F)+δ→(F))+δ¬(F), where δ◦(F) computes the number of occurrences of the connective ◦in F. This measure has the following properties: u(α1)+u(α2)<u(α), u(β1)<u(β), u(β2)<u(β) and u(F)<u(¬¬F). We define the measure function, µT, as the sum of the uniform measure of the formulas in a branch. By the properties of u, the expansion rules reduce the measure of a branch; therefore θi∈rT(θ)=⇒µT(θi)<µ T(θ) (property P1). The uniform notation ensures that an α(β) formula is logically equivalent to the conjunction (disjunction) of its components and a doubly negated formula ¬¬Fis also logically equivalent to F. Hence, if θ;TLwith L=t,itcanbe easily proved that σ|=Tθ⇐⇒ ∃ θi∈L, σ |=Tθi. According to the definition of computation rule, this trivially implies property P3. Finally, we define the model function σTsuch that for every branch θwithout non–literal nor complementary formulas, σT(θ)|=pif and only if pis a positive literal occurring in θ. Obviously if rT(θ)=tthen σT(θ)|=Tθ(property P4). Then, by theorem 1, the algorithm SATTterminates for any formula and is complete and sound. The algorithm applied to the example of figure 1–left performs the following steps (represented as −→ SATT): (p→q)∧p −→ SATTp→q,p −→ SATT −→ SATTp, ¬p,p, q −→ SATTp, q −→ SATTp, q 2.2 Sequents and the Gentzen System We denote sequents as Γ⇒∆, where Γand ∆are lists of formulas. An atomic sequent is a sequent in which every formula is atomic. A valuation σmakes the 1We extend the uniform notation to include equivalence: F↔Gis considered a β–formula with components β1=F∧G,β2=¬F∧¬G, and ¬(F↔G) is considered aβ–formula with components β1=F∧¬G,β2=¬F∧G. sequent Γ⇒∆true if and only if ∃X∈Γ, (σ|=X)∨∃Y∈∆, (σ|=Y). We will consider the axioms and rules of Gentzen System Gpresented in [7], with two additional rules about equivalence: Γ1,F,G,Γ 2⇒∆Γ 1,Γ 2⇒F, G, ∆ Γ1,F ↔G, Γ2⇒∆(↔: left) F,Γ ⇒∆1,G,∆ 2G, Γ ⇒∆1,F,∆ 2 Γ⇒∆1,F ↔G, ∆2(↔: right) In order to prove the satisfiability of a formula F, the rules are applied to the initial sequent F⇒until atomic sequents are obtained. Some atomic sequents provide countermodels of the initial sequent, and hence, models of the original formula. See [7] for more background about the sequent method. We now describe the PTS S=OS,RS,VSassociated with the sequents method. In this PTS, OSis the set of sequents (represented as pairs of lists of formulas), VSis the set of pairs (S, σ) such that σmakes Sfalse and RSthe set of rules given by the following rule schemata: RS1:Γ1,F,Γ 2⇒∆1,F,∆ 2;S RS2:Γ1,¬F,Γ2⇒∆;SΓ1,Γ 2⇒F,∆ RS3:Γ1,F ∧G, Γ2⇒∆;SF, G, Γ1,Γ 2⇒∆ RS4:Γ1,F ∨G, Γ2⇒∆;SF,Γ1,Γ 2⇒∆, G, Γ1,Γ 2⇒∆ RS5:Γ1,F →G, Γ2⇒∆;SΓ1,Γ 2⇒F,∆,G, Γ1,Γ 2⇒∆ RS6:Γ1,F ↔G, Γ2⇒∆;SF, G, Γ1,Γ 2⇒∆, Γ1,Γ 2⇒F, G, ∆ RS7:Γ⇒∆1,¬F,∆2;SF,Γ⇒∆1,∆ 2 RS8:Γ⇒∆1,F ∧G, ∆2;SΓ⇒F,∆1,∆ 2,Γ⇒G, ∆1,∆ 2 RS9:Γ⇒∆1,F ∨G, ∆2;SΓ⇒F, G, ∆1,∆ 2 RS10 :Γ⇒∆1,F →G, ∆2;SF,Γ⇒G, ∆1,∆ 2 RS11 :Γ⇒∆1,F ↔G, ∆2;SF,Γ⇒G, ∆1,∆ 2,G, Γ⇒F, ∆1,∆ 2 RS12 :Γ⇒∆;Stif Γ⇒∆is an atomic sequent and Γ∩∆=Ø The representation function iSbuilds the sequent F⇒for every F∈P(Σ). Thus, σ|=F⇐⇒ σ|=SiS(F) (property P2). We consider any computation rule, rS, such that, for every sequent S,rS(S) is a rule from the above table that can be applied to S. We define the measure function µSas the number of occurrences of propositional connectives in a sequent. The expansion rules reduce this number, therefore Si∈rS(S)=⇒µS(Si)<µ S(S) (property P1). Given an expansion rule S;SLwith L=t, it can be easily proved that σ|=SS⇐⇒ ∃ Si∈L, σ |=SSi. By the definition of computation rule, this implies property P3. Finally, we define the model function σSsuch that for every atomic non– axiom sequent S,σS(S)|=pif and only if poccurs in the left part of S. Obviously, if rS(S)=tthen σS(S)|=SS(property P4). Then, by theorem 1, the algorithm SATSterminates for any formula and is complete and sound. The algorithm applied to the example of figure 1–right performs the following steps (represented as −→ SATS): (p→q)∧p⇒ −→ SATSp→q,p⇒ −→ SATSp⇒p, q,p⇒ −→ SATS −→ SATSq,p⇒ −→ SATSq,p⇒ 2.3 Davis–Putnam Method The Davis–Putnam method is a procedure to decide the satisfiability of a set of clauses. Then, if FC is a procedure to obtain a set of clauses logically equivalent to a formula F, we can use the Davis–Putnam method to decide the satisfiability of F, applying the method to FC(F). See [6] for more background about the Davis–Putnam method. We now describe the PTS D=OD,RD,VDassociated with the Davis– Putnam method. Now, ODis the set of pairs S, M, where Sis a set of clauses and Mis a literal list without complementary literals and such that for every L in M, neither Lnor Lis in some clause in S.VDis the set of pairs (S, M,σ) such that σis model of every clause in Sand every literal in M.RDis the set of rules given by the following rule schemata: RD1:S, M;D if the empty clause is in S RD2:S, L1,...,L n ;DSL,L, L1,...,L n if the unitary clause {L}is in S RD3:S, L1,...,L n ;DSL,L, L1,...,L n,SL,L, L1,...,L n where Lis a literal in a clause in S RD4:,M;Dt where Sis a set of clauses, S, Mand S, L1,...,L n are elements in OD, and SL={C−{L}:C∈Sand L/∈C}and SL={C−{L}:C∈Sand L/∈C}. The representation function iDbuilds a pair FC(F),, where FC is assumed to be a correct procedure to obtain a set of clauses logically equivalent to F, that is, σ|=F⇐⇒ σ|=FC(F)⇐⇒ σ|=DiD(F) (property P2). We consider a computation rule, rD, that applies one of the expansion rules schemata in the following preference order RD1,RD2,RD3and RD4. We define the measure function µD, such that, for every pair S, M∈O D, µD(S, M) is the total number of literals of the clauses of S. The expansion rules reduce this value, therefore Si,M i∈rD(S, M)=⇒µD(Si,M i)< µD(S, D) (property P1). Given an expansion rule S, M;DLwith L=t, it can be easily proved that σ|=DS, M⇐⇒∃Si,M i∈L, σ |=DSi,M i. By the definition of computation rule, this implies property P3. Finally, we define the model function σDsuch that for every pair ,Mand p∈Σ,σD(,M)|=pif and only if p∈M. Obviously, if rD(S, M)=tthen σD(S, M)|=DS, M(property P4). Then, by theorem 1, the algorithm SATDterminates for any formula and is complete and sound. The algorithm applied to the formula (p→q)∧pperforms the following steps (represented as −→ SATD): {¬p, q},{p}, −→ SATD{q},p −→ SATD −→ SATD,q,p −→ SATD,q,p 3 Formalizing the Generic SAT–Prover in ACL2 Let us see in this section how we formalize the concepts and results of the previous section in the ACL2 logic.The ACL2 logic is a quantifier–free, first–order logic with equality, describing an applicative subset of Common Lisp. The syntax of terms is that of Common Lisp. The logic includes axioms for propositional logic and for a number of Lisp functions and data types. Rules of inference include those for propositional calculus, equality, and instantiation, as well as the introduction of new total recursive functions by the principle of definition (using defun) and constrained functions (via encapsulate). The ACL2 theorem prover mechanizes that logic, being particularly well suited for obtaining automatized proofs based on simplification and induction. For a detailed description of ACL2, we refer the reader to the ACL2 book [8]. 3.1 Definition of the Generic Algorithm Before reasoning in ACL2 about the algorithm SATG, we have to define in the ACL2 logic the functions introduced by the generic framework presented in section 2. These ACL2 functions and their intended meanings are shown in the following table: gen-object-p(O)O∈O gen-repr(F)i(F) gen-comp-rule(O)r(O) gen-dist-val(σ, O)σ|=GO gen-model(O)σ(O) gen-measure(O)µ(O) gen-select(lst) selects an element from a list lst These functions are not introduced in the ACL2 logic using the principle of definition. Since they are generic, we define them by means of the encapsulate mechanism, which allows the user to introduce new function symbols by axioms constraining them to have certain properties (to ensure consistency, a witness local function having the same properties has to be exhibited). Inside an encapsulate, the properties stated need to be proved for the local witnesses, and outside, they work as assumed axioms. In this case, the properties about the generic functions are the following2: Theorem: gen-object-p-gen-repr propositional-p(F)→gen-object-p(gen-repr(F)) Theorem: gen-object-p-gen-comp-rule gen-object-p(O1)∧(O2∈gen-comp-rule(O1)) →gen-object-p(O2) 2The expressions provided to ACL2 are written in Common Lisp notation but, to improve their legibility, we present them using a infix notation. Theorem: e0-ordinalp-gen-measure e0-ordinalp(gen-measure(O)) Theorem: P1 O2∈gen-comp-rule(O1) →gen-measure(O2)<gen-measure(O1) Theorem: P2 propositional-p(F) →(gen-dist-val(σ,gen-repr(F)) ↔models(σ,F)) Definition: gen-dist-val-lst(σ,O-lst)= if endp(O-lst)then nil else gen-dist-val(σ,car(O-lst)) ∨gen-dist-val-lst(σ,cdr(O-lst)) fi Theorem: P3 gen-object-p(O)∧(gen-comp-rule(O)=t) →(gen-dist-val-list(σ,gen-comp-rule(O)) ↔gen-dist-val(σ,O)) Theorem: P4 gen-object-p(O)∧(gen-comp-rule(O)=t) →gen-dist-val(gen-model(O), O) Theorem: gen-select-member consp(lst)→(gen-select(lst)∈lst) The first three properties state that the functions gen-repr,gen-comp-rule and gen-measure take values as expected, when acting on elements of their intended domains. The properties named P1,P2,P3 and P4 are the corresponding formalization of the properties P1,P2,P3and P4, respectively, as defined in the hypothesis of theorem 1 3. The symbol <denotes the “less than” relation between ordinals. Finally, note that we also introduce a function gen-select, that selects an element from any non–empty list. This function is needed in the definition of the generic SAT algorithm. Once the functions of our generic framework have been (abstractly) defined, we define in ACL2 the function generic-sat, implementing the algorithm SATG: 3The functions propositional-p and models are defined in a previous ACL2 formalization about the syntax and semantics of propositional logic; they define, respectively, the propositional formulas and models of formulas. The function gen-dist-val-lst can be seen as a generalized disjunction of the predicate gen-dist-val acting on the objects of a list. without repeating the main proof effort and allowing some kind of mechanization of the process. We have used this methodology to develop resolution based SAT–provers: we have defined a generic resolution procedure and we have proved its termination, soundness and completeness properties. The completeness proof is based on the developed by Bezem in [2]. This work can be found in [10]. An additional step in this methodology could be refinement. We could define more efficient functions and obtain their properties by proving equivalence theorems with the less efficient ones. In this line of work we have implemented a DPLL (Davis Putnam Logemann Loveland) procedure in ACL2, based on [15], which turns out to be much more efficient than the one presented here (It solves the 7-queens problem in 0.010 seconds and the 16-queens problem in 0.750 seconds). Using this technique of refinement, we could verify this more efficient version of the Davis–Putnam procedure Another line of work is to apply the generic framework to other SAT methods (KE, TAS-D [1], etc). Finally, we also plan to use the same methodology to develop generic framework for non–classical and first–order logics. In the last case, we think that the development of a generic framework could be easy, combining the results presented here with a verified unification algorithm, such as the algorithm presented in [13] and [11]. References 1. G. Aguilera, I.P. de Guzman, M. Ojeda–Aciego and A. Valverde. Reductions for non-clausal theorem proving. Theoretical Computer Science 266, pages 81–112. Elsevier, 2001. 2. M. Bezem. Completeness of resolution revisited. Theoretical Computer Science 74, no. 2, pages 227–237, 1990. 3. R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, 1979. 4. J. Caldwell. Decidability Extracted: Synthesizing “Correct-by-Construction” Decision Procedures from Constuctive Proofs. PhD thesis, Cornell University, 1998 5. N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. In Proceedings of the Sixth International Colloquium on Automata, Languages and Programming, LNCS 71, pages 188–202. Springer–Verlag, 1979. 6. M.C. Fitting. First–Order Logic and Automated Theorem Proving. Springer– Verlag, New York, 1990. 7. J.H. Gallier. Logic for Computer Science, Foundations of Automatic Theorem Proving. Harper and Row Publishers, 1986. 8. M. Kaufmann, P. Manolios, and J S. Moore. Computer–Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000. 9. F.J. Martin–Mateos, J.A. Alonso, M.J. Hidalgo, and J.L. Ruiz–Reina. A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory, 2002. 10. F.J. Martin–Mateos. Teoria computacional (en ACL2) sobre calculos proposicionales. PhD thesis, University of Seville, 2002. 11. J.L. Ruiz–Reina. Una teoria computacional acerca de la logica ecuacional. PhD thesis, University of Seville, 2001. 12. J.L. Ruiz–Reina, J.A. Alonso, M.J. Hidalgo, and F.J. Martin. Multiset Relations: a Tool for Proving Termination. In Second ACL2 Workshop, Technical Report TR-00-29, Computer Science Departament, University of Texas, 2000. 13. J.L. Ruiz–Reina, J.A. Alonso, M.J. Hidalgo, and F.J. Martin. Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover. In Proceedings AGP’99, Joint Conference on Declarative Programming, L’Aquila (Italia), 1999. 14. R.M. Smullyan. First–Order Logic. Springer–Verlag: Heidelberg, Germany, 1968. 15. H. Zhang and M.E. Stickel. Implementing the Davis–Putnam method Journal of Automated Reasoning, 24(1–2):277–296, 2000.