Formal verification of a generic framework to synthesize SAT-provers

Formal verification of a generic framework to synthesize SAT-provers Francisco–Jes´us Mart´ın–Mateos, Jos´e–Antonio Alonso, Mar´ıa–Jose´ Hidalgo and Jos´e–Luis Ruiz–Reina Computational Logic Group Dept. of Computer Science and Artificial Intelligence, University of Seville E.T.S.I. Inform´atica, Avda. Reina Mercedes, s/n. 41012 Sevilla, Spain E-mails: {fmartin,jalonso,mjoseh,jruiz}@cs.us.es Abstract. We present in this paper an application of the ACL2 system to generate and reason about propositional satisfiability provers. For that purpose, we develop a framework where we define a generic SAT-prover based on transformation rules, and we formalize this generic framework in the ACL2 logic, carrying out 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 automated way. Three instantiations of the generic framework are considered: semantic tableaux, sequent and Davis–Putnam–Logeman–Loveland methods. 1. Introduction A common practice in program verification is stepwise refinement. This means that essential properties of programs can be first proved at a very abstract level, considering only a generic specification of the program, skipping technical details of concrete implementations. Thus, the properties proved can be deduced for a given implementation of the generic specification, by simply showing that this implementation is a concrete instance of the generic procedure. Further refinements of the implementations (in order to obtain better performance) can still be verified by showing that they compute the same results as an-other verified implementation. In this paper, we describe an application of this technique to reason formally about a family of propositional satisfiability (SAT) decision procedures, using the ACL2 system. SAT provers are an important component of many applications in theorem proving in particular and artificial intelligence in general [9], so it makes sense the development of formally verified SAT decision procedures, as a way of certifying this “proof engine” component [18]. The reason why we have chosen ACL2 as the logic and prover used to reason about this procedures, is that this system provides a framework ∗ This work has been supported by project TIC2000-1368-C03-02 (Ministry of Science and Technology, Spain), cofinancied by FEDER founds. 2 where reasoning and computing can be done. ACL2 [12] is a programming language, a logic for reasoning about programs in the language, and a theorem prover supporting formal reasoning in the logic. So the procedures can be implemented, executed and formally verified in the same system. Three case studies are considered: semantic tableaux, sequent calculus and the Davis–Putnam–Logeman–Loveland method. The common pattern of all these SAT 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 SATprover 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. As a byproduct, we have developed a tool to make the instantiation process more convenient, obtaining in an automated way the concrete and executable procedures and the instances of the theorems proved for the generic framework. This paper is an extended and revised version of [15]. It 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–Logeman–Loveland method) can be placed into the generic framework. In Section 3 we show how this framework has been formalized in ACL2 and how its main properties has been proved. In Section 4 we describe how these generic definitions and theorems has been instantiated, to obtain verified and executable Common Lisp definitions of tableaux based, sequent based and Davis–Putnam– Logeman–Loveland SAT-provers. Finally, in Section 5 we draw some conclusions. Due to the lack of space we will skip details of the mechanical proofs and for the same reason some function definitions will be omitted. The complete formalization is available in [16]. 2. A generic framework to develop propositional SAT-provers Analyzing some well-known methods of proving propositional satisfiability (such as sequent, tableaux or Davis–Putnam–Logeman– Loveland), 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 3 (p→q)∧p T1 (p→q)∧p p→q p T2  Q Q (p→q)∧p p→q p ¬p q T3  Q Q H H   (p→q)∧p p→q p ¬p q σ(p) = 1 σ(q) = 1 Figure 1. An example of tableaux method 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 must point out that these objects are not only theoretical structures used to describe the method (e.g. lists or sets of formulas), but they can be real data structures used in the implementation (e.g. arrays, linked lists, hash tables, ...) of the SAT procedures. We can see this behavior in the semantic tableaux method, by means of the example shown in Figure 1. From the formula (p→q)∧pthe initial tree T1with a single node is built. In a first step the formula is expanded obtaining one extension with two formulas p→qand p (tree T2). In a second step the formula p→qis expanded obtaining two extensions, the first with the formula ¬pand the second with the formula q(tree T3). The left branch becomes closed (i.e., 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. Our goal in this section is to describe a generic framework where these methods can be fit. First we introduce some notation. We consider an infinite set of proposition 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 ↔. The complement of a formula F, denoted as F, is defined such that F=G if F=¬G, and F=¬Fotherwise. A literal is a formula por ¬p, where p∈Σ. A clause is a finite sequence of literals. A valuation is a function 4 σ: Σ −→ 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 of a clause C, if it is a model of some literal in C. The capital Greek letters Γ and ∆ (possibly with subscripts) denote finite sequences of formulas (we sometimes use the term list instead of finite sequence). We will use the notation he1, ..., ekito represent a finite sequence, and O∗to denote the set of finite sequences of elements of the set O. We say that xis a member of the list he1, ..., eki, denoted as x∈ he1, ..., eki, if ∃i, 1≤i≤n, such that x=ei. We write hΓ1, F, Γ2ior Γ1, F, Γ2, to distinguish the formula Fin a sequence of formulas. Finally, Ord denotes the class of all ordinals. 2.1. A generic algorithm for proving propositional satisfiability DEFINITION 1. APropositional Transformation System (PTS, for short) is a triple G=hOG,;G,|=Gi, where OGis a set, and ;Gand |=Gare binary relations such that ;G⊆ O×(O∗∪{t})and |=G⊆VΣ×O. We will call OGthe set of propositional objects (or simply objects) and ;Gthe set of expansion rules. Intuitively, the objects are the structures used by a propositional SAT-prover and the expansion rules describe the steps that it performs. Note that we allow rules of the form O;Ghi and rules of the form O;Gt. The first one represents dead ends in the search for satisfiability, and the second one represents successful ends. When σ|=GO, we say that σis a distinguished valuation for O. The idea is that when a successful end is found, the distinguished valuations for the last object provide a model of the original formula. Intuitively, the relation |=Gtranslates the relation |= from formulas to the objects used by the SAT-prover. DEFINITION 2. Given a PTS G=hOG,;G,|=Gi: 1. A computation rule is a function r:O −→ O∗∪ {t}such that r⊆;G. 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}. 5 Given a PTS G=hOG,;G,|=Gi, a computation rule rand a representation function i, we define the following algorithm SATGfor proving satisfiability of a propositional formula. ALGORITHM 1 (SATG). The input to this algorithm is a propositional formula Fand it proceeds as follows: 1. Let L=hi(F)i. 2. While Lis a non-empty list, do: Select Oja member of the list L=hO1, ..., Oni. a) If r(Oj) = t, then stop and return hOji. b) If r(Oj) = hO0 1, ..., O0 mi(m≥0), then let L=hO0 1, ..., O0 m, O1, ..., Oj−1, Oj+1, ..., Oni. 3. Return f. The intuitive idea is simple: given F, we start with the initial object i(F) and repeatedly apply the expansion rules until tis obtained or until there are no more objects left. Termination of this process will be guaranteed by a measure function µ. The strategy to apply the rules is determined by the given computation rule rand by the selection strategy of objects of the list L. Note that assuming the existence of a computation rule means that for every object there is at least one rule that can be applied to it. It can be proved that under some conditions that we give below, if tis obtained from an object Oj, then we can obtain a distinguished valuation using a model function and this valuation turns out to be a model of the original formula. Under the same conditions, if fis obtained, the original formula is unsatisfiable. DEFINITION 3. We say that SATGis complete if for all F∈P(Σ) such that ∃σ∈VΣ:σ|=F, then SATG(F)6=f. We say that it is sound if for all F∈P(Σ) such that SATG(F)6=f, then ∃σ∈VΣ:σ|=F. THEOREM 1. Let G=hOG,;G,|=Gibe a PTS, ra computation rule, ia representation function, µa measure function and γa model function, such that the following properties hold: P1:Oi∈r(O) =⇒µ(Oi)< µ(O) P2:F∈P(Σ) =⇒(σ|=F⇐⇒ σ|=Gi(F)) P3:O∈ O ∧ r(O)6=t=⇒(σ|=GO⇐⇒ ∃Oi∈r(O), σ |=GOi) 6 P4:O∈ O ∧ r(O) = t=⇒γ(O)|=GO then the algorithm SATGterminates for any formula and is complete and sound. Furthermore, if SATG(F) = hOithen γ(O)|=F. Termination Proof. In the termination proof of SATG, we will use a multiset relation built from the measure function. Roughly speaking, a finite multiset over Ais a subset of A“with repeated elements”. Let us briefly recall the notion of multiset relation. Given a relation <on a set A, we define the multiset relation induced by <on the set of finite multisets over A, denoted as <mul, in the following way: N <mul M if there exist X, Y finite multisets over A, such that Ø 6=X⊆M, N= (M\X)∪Yand for all y∈Ythere exists x∈Xsuch that y < x. Intuitively, this means that a smaller multiset can be obtained by removing a non-empty subset of elements, and adding elements which are smaller than some element removed. In [7] it is proved that <mul is well-founded whenever <is well-founded. Let us now prove the termination of SATG. For that purpose, we must prove that point 2 is a finite loop. Assume that the list of objects in point 2 is hO1, ..., Oni, the selected element is Ojand r(Oj) = hO0 1, ..., O0 mi, with m≥0. 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,O0 k<µOjby P1. Therefore, the multiset {O0 1, ..., O0 m, O1, ..., Oj−1, Oj+1, ..., On}is smaller than {O1, ..., On}with respect to the multiset extension of <µ(which is also well-founded). 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, since the algorithm terminates, in some step an object O0such that r(O0) = twill be considered. Then SATG(F) = hO0i 6=f. Soundness Proof. If SATG(F) = hOithen r(O) = tand, by P4, γ(O)|=GO. Then, by the property noted in the completeness proof, in every list considered in point 2 exists O0such that γ(O)|=GO0. Therefore, this holds for the initial list considered hi(F)i, i.e., γ(O)|=G i(F), and, by P2,γ(O)|=F. 7 2.2. Semantic Tableaux We now show how the semantic tableaux method can be seen as a propositional transformation system, and how a simple SAT-prover based on this method can be seen as a particular instance of the algorithm SATG. Let us first overview the propositional tableaux method, following the description given in [8]. This method is a refutation system: to prove that a formula Fis valid, it starts with a finite tree with only one node labeled with ¬Fand applies a set of expansion rules until it generates a contradiction. From a more constructive point of view, the method tries to build a model of the formula ¬F. If this is not possible, then Fis valid. The tableaux expansion rules are concisely presented using the uniform notation [19]1. Using this notation, non-literal formulas are classified as doubly negated, α-formulas or β-formulas, as we show in the following tables: Double negation component ¬¬X X α α1α2 X∧Y X Y ¬(X∨Y)¬X¬Y ¬(X→Y)X¬Y β β1β2 X∨Y X Y ¬(X∧Y)¬X¬Y X→Y¬X Y X↔Y X ∧Y¬X∧ ¬Y ¬(X↔Y)X∧ ¬Y¬X∧Y Note that the α-formulas are equivalent to the conjunction of their components α1and α2, the β-formulas are equivalent to the disjunction of their components β1and β2, and the doubly negated formulas are equivalent to their unique component. The method acts as follows. Let Tbe a finite tree, with its nodes labeled with propositional formulas, and θa branch in Twith an occurrence of a non-literal formula F. If Fis ¬¬X, then the branch θis extended adding a new node labeled with X. If Fis an α-formula, then the branch θis extended adding two nodes labeled with the components α1and α2of the formula. If Fis a β-formula, then the branch θis extended producing two branches at the end, each one with a node labeled, respectively, with the components β1and β2of the formula. A branch θis (atomically) closed if there exist two nodes in θlabeled with complementary (literal) formulas. The method is applied until 1We extend the uniform notation to include equivalence. 8 every branch is closed. In this case the original formula Fis valid. If there is a non closed branch θsuch that every occurrence of a non-literal formula in θhas been expanded, then the formula ¬Fhas a model and the formula Fis not valid. In this case a model of ¬Fcan be built from the literal formulas in θand we say that θprovides a model. See Figure 1 for an example. We now describe the PTS T=hOT,;T,|=Tiassociated with the semantic tableaux method. In this PTS, OTis the set of finite sequences of formulas (representing tableaux branches), σ|=Tθif and only if σmakes true every formula in the branch θ, and ;Tis the relation described by the following rule schemata: RT1:hΓ1, G, Γ2,¬G, Γ3i;Thi RT2:hΓ1,¬G, Γ2, G, Γ3i;Thi RT3:hΓ1,¬¬G, Γ2i;ThhΓ1, G, Γ2ii RT4:hΓ1, α, Γ2i;ThhΓ1, α1, α2,Γ2ii RT5:hΓ1, β, Γ2i;ThhΓ1, β1,Γ2i,hΓ1, β2,Γ2ii RT6: Γ ;Ttif Γ does not have non-literal nor complementary formulas The rule schemata RT3,RT4and RT5correspond with the tableaux expansion rules presented above. The rule schemata RT1and RT2 check if a branch is closed and the rule RT6checks if a branch provides a model. Given concrete representation, computation rule, measure and model functions for this PTS, we define a propositional tableaux method, which we call SATT, as a concrete version of the generic procedure SATG. By Theorem 1, this procedure will be sound and complete if properties P1to P4are verified. We now define these four functions, proving the properties in passing. The representation function iTis defined such that for every F∈ P(Σ), iT(F) = hFi; that is, the only branch in the initial tree considered by the semantic tableaux method. Obviously, σ|=F⇐⇒ σ|=Ti(F) (property P2). We can consider any computation rule, rT, such that, for every branch θ,rT(θ) is the result of applying one of the above rule schemata to θ, whenever such rule may be applied. Several versions of the semantic tableaux method could be represented by different computation rules. For example, if the rule schemata RT1and RT2have less priority than the others, then the expansion rules are applied until every branch is atomically closed. To finish the expansion process when the branches are closed, the rule schemata RT1and RT2should have higher priority than the others. Another point could be the preference order between the rule schemata RT3and RT4, without bifurcation, and the rule schemata RT5, with makes a bifurcation. Taking into account 9 these ideas, we can define several computation rules and hence, several propositional theorem provers based on semantic tableaux associated with the above PTS. In order to define the measure function, we define the uniform measure [1]2, 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(X)< u(¬¬X). 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 ¬¬Xis also logically equivalent to X. Hence, if θ;TLwith L6=t, it can be easily proved that σ|=Tθ⇐⇒ ∃θi∈L, σ |=Tθi. According to our 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 performs the following steps (represented as 7−→ SATT): hh(p→q)∧pii 7−→ SATThhp→q, pii RT3 7−→ SATThhp, ¬pi,hp, qii RT2 7−→ SATThhp, qii RT1 7−→ SATThhp, qii RT5 The set of rule schemata proposed could be improved to obtain a more efficient propositional theorem prover from the associated PTS. For example, the rule schemata RT1could be mixed with the rule schemata RT2,RT3and RT4to avoid occurrences of complementary formulas. Following this idea, we have defined another PTS T0= hOT0,;T0,|=Tiassociated with the semantic tableaux method in which the propositional objects are lists of formulas without complementary elements and the rule schemata are the following: RT01:hΓ1,¬¬G, Γ2i;T0hi if G∈ hΓ1,Γ2i RT02:hΓ1,¬¬G, Γ2i;T0hhΓ1, G, Γ2ii if G6∈ hΓ1,Γ2i 2We extend the measure provided in [1] to include equivalence. 16 PTS. For example, the rule RD4could be changed to detect the end of the reduction process when a set of clauses Sonly has pure literals (those that only appear positive or negative in the set of clauses) and the rule RD3could be changed to choose only non-pure literals. 3. Formalizing the generic SAT-prover in ACL2 Now we describe a tool based on the theoretical development presented in Subsection 2.1. This tool builds a certified propositional theorem prover from a Propositional Transformation System and its associated functions as it was described in Algorithm 1, whenever the properties P1,P2,P3and P4are satisfied. It is built on top of the ACL2 system. In this section, we show how the generic development of Subsection 2.1 is formalized in ACL2. 3.1. A brief introduction to ACL2 ACL2 is a programming language, a logic for formal reasoning about programs defined in the programming language, and a theorem prover supporting mechanized reasoning in the logic. It is developed by J Moore and Matt Kaufmann in the University of Texas at Austin, considered as an “industrial-strength” successor of Nqthm, also known as the Boyer-Moore theorem prover. As a programming language, ACL2 is an extension of a subset of Common Lisp, containing most of the applicative part of that language. The ACL2 logic is a quantifier-free, first-order logic with equality, describing the functions of the programming language. The syntax of terms is that of Common Lisp and the logic includes axioms for propositional logic and for a number of Lisp functions and data types. Rules of inference of the logic include those for propositional calculus, equality and instantiation. One important rule of inference is the principle of induction, that permits proofs by well-founded induction on the ordinal ε0. The theory has a constructive definition of the ordinals up to ε0, in terms of lists and natural numbers, given by the predicate e0-ordinalp and the order e0-ord-<. By the principle of definition (using defun), new function definitions are admitted as axioms only if there exists a measure in which the arguments of each recursive call decrease with respect to a well-founded relation, ensuring in this way that no inconsistencies are introduced by new definitions. Some higher order functionality is provided by means of the encapsulate mechanism [13] which allows the user to introduce new 17 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. This mechanism behaves like an universal quantifier over a set of functions abstractly defined with it. A derived rule of inference, called functional instantiation, gives some features of a higher order logic by allowing to instantiate the function symbols of a previously proved theorem, replacing them with other function symbols or lambda expressions, provided it can prove that the replacements satisfy the constraints on the old symbols. The ACL2 theorem prover mechanizes the logic. The prover is mainly based on applying simplification and induction. Roughly speaking, when the prover tries to prove a conjecture, it simplifies the formula. If it obtains t, then the conjecture is proved. Otherwise, it guesses an (often suitable) induction scheme, and recursively tries to prove the subgoals generated. The theorem prover is automatic in the sense that once submitted a conjecture (by the command defthm), the user can no longer interact with the system. But in a wider sense, the prover is interactive: nontrivial results often fail to be proved unless the user previously proves lemmas that can be used in subsequent proofs as rewriting rules. In this way, the user can help the prover to find a preconceived hand proof. This is the way we have interacted with the system to obtain the results presented in this section. For a detailed description of ACL2, we refer the reader to the ACL2 book [11]. 3.2. Definition of the generic algorithm The first step to reason in ACL2 about the algorithm SATG, is to define in the ACL2 logic the functions introduced by the generic framework presented in Section 2.1. The names of 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 18 of the encapsulate mechanism, constraining them to have certain properties3. In this case, the properties about the generic functions are the following4: Assumption: gen-object-p-gen-repr propositional-p(F)→gen-object-p(gen-repr(F)) Assumption: gen-object-p-gen-comp-rule gen-object-p(O1)∧(O2∈gen-comp-rule(O1)) →gen-object-p(O2) Assumption: e0-ordinalp-gen-measure e0-ordinalp(gen-measure(O)) Assumption: P1 O2∈gen-comp-rule(O1) →gen-measure(O2)<gen-measure(O1) Assumption: P2 propositional-p(F) →(gen-dist-val(σ,gen-repr(F)) ↔models(σ,F)) Assumption: P3 gen-object-p(O)∧(gen-comp-rule(O)6=t) →(gen-dist-val(σ,O) ↔gen-dist-val-list(σ,gen-comp-rule(O))) Assumption: P4 gen-object-p(O)∧(gen-comp-rule(O) = t) →gen-dist-val(gen-model(O), O) Assumption: 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. 3The local witnesses are irrelevant to the definition of the generic algorithm and the proof of its properties, so we omit them here. 4The expressions provided to ACL2 are written in Common Lisp notation but, to improve their legibility, we present them here using a “infix” notation. 19 The 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-list can be seen as a generalized disjunction of the predicate gen-dist-val acting on the objects of a list. 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 introduced, we define in ACL2 the function generic-sat, implementing the algorithm SATG: Definition: generic-sat-lst(O-lst) = if endp(O-lst)then nil (1) else let* Obe gen-select(O-lst), (2) rest be remove-one(gen-select(O-lst), O-lst), expansion be gen-comp-rule(O) (3) in if expansion =t then list(O) (4) else generic-sat-lst(expansion @rest) Measure: gen-measure-lst(O-lst) Well founded relation: <mul Definition: generic-sat(F) = generic-sat-lst(list(gen-repr(F))) where the symbol @ is the “append” operation between lists. Note that the main function of this algorithm is given by the recursive function generic-sat-lst, acting on a list of objects to be expanded. This function implements the while loop in the definition of SATG. The termination of this loop is justified by the measure gen-measure-lst(O-lst) and the multiset well-founded relation <mul. We will explain more about this issue in the next subsection. When a rule of the form hO, tiis applied to a selected object O, the algorithm returns a singleton list containing O(4). According to the property assumed about the function gen-model, this object has a distinguished valuation. Thus, returning the object is useful to provide a model of the input formula. On the other hand, when there are no more objects to be expanded, the algorithm returns f, represented as the ACL2 symbol nil (1). This algorithm is left unspecified in two aspects: first, no concrete computation rule is defined by the generic function gen-comp-rule (3); 20 second, the object to which the expansion rule is applied, selected by the abstractly defined function gen-select, is not specified (2). 3.3. Termination As it was pointed out in Subsection 3.1, new function definitions are admitted in ACL2 only if there exists a well-founded measure in which the arguments of each recursive call decrease. In the case of the function generic-sat-lst the heuristics of ACL2 are not able to find a suitable termination argument, so we must explicitly provide a measure on its argument an show that this measure decreases in every recursive call with respect to a well-founded relation. The only predefined well-founded relation in ACL2 is e0-ord-<, implementing the usual order between ordinals less than ε0. The function e0-ordinalp recognizes those ACL2 objects representing such ordinals. If we want to define a new well-founded relation in ACL2, we have to explicitly provide a monotone ordinal function, and prove the corresponding order-preserving theorem (see [11] for details). To show termination of generic-sat-lst, we follow the lines described in the informal proof given in Section 2.1. The measure associated to its argument is given by a function gen-measure-lst that computes the list of the ordinal measures of the objects of a given list. This measure decreases with respect to the multiset relation induced by e0-ord-<. Since e0-ord-< is well-founded, so is its induced multiset relation [7]. A formal proof of the well-foundedness of the multiset relation induced by given well-founded relation was formalized in the ACL2 logic in [17], where the defmul tool was also developed. This tool automatically generates the definitions and prove the theorems needed to introduce in ACL2 the multiset relation induced by a given well-founded relation. In our case, we only need the following defmul call: (defmul (e0-ord-< nil e0-ordinalp e0-ord-<-fn nil nil)) This automatically generates the definition of mul-e0-ord-<, (denoted as <mul in the following), implementing the multiset relation on finite multisets (lists) of ordinals induced by the relation e0-ord-<. And it also automatically proves the theorems needed to introduce this relation as a well-founded relation in ACL2. See details about the defmul syntax in [17]. The main termination property of generic-sat-lst is given by the following theorem, establishing that the measure gen-measure-lst decreases in every recursive call with respect to the well-founded relation <mul: 21 Theorem: generic-sat-lst-termination-property let* Obe gen-select(O-lst), rest be remove-one(gen-select(O-lst), O-lst), expansion be gen-comp-rule(O) in consp(O-lst)∧(expansion 6=t) →gen-measure-lst(expansion @rest) <mul gen-measure-lst(O-lst) Having proved this theorem (and given that <mul is well-founded, as it was automatically proved by the above call to defmul) the definition of generic-sat-lst is shown to be terminating and it is admitted in the logic (and therefore, the definition of generic-sat). 3.4. Soundness and completeness The following theorems establish the formal properties of the function generic-sat (soundness and completeness): Theorem: soundness-generic-sat propositional-p(F)∧generic-sat(F) →models(generic-mod(F), F) Theorem: completeness-generic-sat propositional-p(F)∧models(σ,F)→generic-sat(F) Due to the lack of existential quantification in the ACL2 logic, the soundness theorem has to be formulated by explicitly giving a model of the formula F. This model can be easily obtained from the result returned by the generic-sat procedure, as defined by the function generic-mod: Definition: generic-mod(F) = if consp(generic-sat(F)) then gen-model(first(generic-sat(F))) else nil The above two theorems formalize Theorem 1 in ACL2. They are proved along the lines of the informal proof given in Section 2.1, basically first proving by induction analogous properties about generic-sat-lst. Of course, the properties assumed about the generic functions showed in the Subsection 3.2 play a crucial role. See details of the mechanical proof in [16]. 22 4. Instantiating the generic framework Concrete SAT-provers will be given by defining concrete counterparts of the abstractly defined functions given in Subsection 3.2. With these concrete functions, one can define concrete versions of the algorithm generic-sat. We can also obtain concrete versions of the termination, soundness and completeness theorems: if the assumed properties about the generic functions are verified by the concrete functions, then by functional instantiation we can easily conclude termination, soundness and completeness of the concrete SAT-prover. 4.1. An overview of the instantiation process We describe in this section how we perform the instantiation process in order to obtain a certified specific SAT-prover as a concrete instantiation of the generic framework. First of all, we need a concrete version of the generic functions given in Subsection 3.2. Let us assume, for example, that we have a PTS such that its associated functions are given by functions named object-p,repr,comp-rule,dist-val,model, measure and select, concrete counterparts of the generic functions defined in Subsection 3.2, and reflecting the given PTS. We also need the functions dist-val-list, a generalized disjunction of the predicate dist-val over a list of objects, and object-list-p, a recognizer for proper (null terminated) lists of objects. The following steps would have to be performed in order to obtain a certified SAT-prover: 1. The above concrete counterparts of the generic functions have to be defined in ACL2. We will assume that these functions are executable (that is, they are not defined via encapsulate). 2. Concrete versions of the assumed properties about the generic functions (given in Subsection 3.2) have to be proved. 3. The concrete counterparts of the derived functions (with the final goal of defining the concrete version of the function generic-sat), have to be defined. Note that these functions will be executable. 4. Finally, concrete versions of the termination, soundness and completeness theorems have to be formulated and proved by functional instantiation from the generic theorems. The same procedure would have to be done for every concrete instantiation of the generic framework, so it makes sense to use a tool to 23 mechanize this process to some extent. In particular, the last two steps can be completely automated. In [14], we describe a user tool that we developed to instantiate generic ACL2 theories. This tool turns out to be a valuable help in this context, where we have developed a generic theory about SAT-provers and we want to instantiate the theory to obtain concrete, formally verified and executable SAT-provers. This tool mainly consists of a macro named def-generic-theory, which receives as argument a string identifying the theory and a sequence of ACL2 events (definitions and theorems), some of which are labeled to be instantiated. When an ACL2 book5developing a generic theory is created, we include a call to this macro. The effect of the macro call is to define another macro that automatically builds concrete events as instances of the generic events, and to instruct the prover to establish the generated theorems by functional instantiation of the generic ones (thus, they are automatically proved). For example, in the book that formalizes the generic framework for SAT-provers (as described in the previous section), we include the following: (def-generic-theory *generic-sat* <events>) Here <events> is a sequence containing the events corresponding to the generic definitions and theorems that can be instantiated by other ACL2 books. In particular, the definition of generic-sat and the theorems establishing its properties. When this macro call is executed, it defines a new macro that receives as input a functional substitution, generates the corresponding functional instantiation of the instantiable events. For example, once the functions implementing the concrete counterparts of the generic functions are defined and we have proved that they verify the assumed properties, we include the book with the generic SAT-prover formalization. At that point, a macro definstance-*generic-sat* is automatically defined, and we can use this macro to automatically generate instantiated events for the concrete SAT-prover, as follows: (definstance-*generic-sat* ((gen-object-p object-p) 5A collection of ACL2 definitions and proved theorems is usually stored in a certified file of events (a book in the ACL2 terminology), that can be included in other books. 24 (gen-object-list-p object-list-p) (gen-repr repr) (gen-dist-val dist-val) (gen-dist-val-list dist-val-list) (gen-comp-rule comp-rule) (gen-select select) (gen-measure measure) (gen-model model)) "-concrete") Note that this macro receives as input a functional substitution, associating every function of the generic framework with its concrete counterpart. Note that the functions object-list-p and dist-val-list must also be included. It also receives a string, used to name the new events generated, by appending it to the name of the original event. For example, in the above call, we used the prefix "-concrete". The result of this macro call is the automatic generation of the events needed to define and verify in ACL2 the concrete SAT-prover. As a consequence, the definition of a function named generic-sat-concrete is generated, as a functional instance of generic-sat. And also the following theorems, establishing the soundness and completeness of generic-sat-concrete, are automatically generated and proved: Theorem: soundness-generic-sat-concrete propositional-p(F)∧generic-sat-concrete(F) →models(generic-mod-concrete(F), F) Theorem: completeness-generic-sat-concrete propositional-p(F)∧models(σ,F) →generic-sat-concrete(F) Note that, once the concrete counterparts of the generic functions verifying the properties showed in Subsection 3.2 are proved, no additional interactive proof effort is needed to define and verify the concrete and executable SAT-prover. 4.2. A tableaux based SAT-prover Along the lines of Subsection 2.2, we have defined in ACL2 several tableaux based instantiations of the generic framework. For that purpose we have defined a tableaux version of the generic functions given in Subsection 3.2: tableaux-object-p,tableaux-repr, 25 tableaux-comp-rule,tableaux-dist-val,tableaux-model, tableaux-measure and tableaux-select. For the first tableaux based SAT-prover, these functions are defined as suggested in Subsection 2.2. For example, the definition of the computation rule is the following (recall that in this case, objects are lists of propositional formulas, representing branches in a tableau): Definition: tableaux-comp-rule(θ) = if closed-tableau(θ)then nil RT1 else let Fbe one-formula(θ) θ0be remove(F,θ) in if doubly-neg-p(F) then list(add(neg-neg-component(F),θ0)) RT2 elseif alfa-formula-p(F) then list(add(component-1(F), add(component-2(F),θ0)))) RT3 elseif beta-formula-p(F) then list(add(component-1(F),θ0)), add(component-2(F),θ0))) RT4 else t RT5 Here the function closed-tableau checks if a branch has complementary formulas. In this case, the empty list is returned. Otherwise, a formula is selected using the function one-formula, and the branch is expanded according to the type of the formula selected, as described by the rules ;T. Note that this computation rule implements a strategy for applying the tableaux expansion rules in a preference order. This order is implicitly given by the function one-formula. Any other strategy could have been defined, provided that the properties assumed about the generic functions could be proved for the concrete counterparts. In this case, these properties are proved easily, except for P3 and P4, which are somewhat more elaborate. Once the assumed properties in the generic framework have been proved for the tableaux case, we can automatically instantiate the generic SAT-prover algorithm as we have described in the previous subsection. As a result, we obtain a certified function implementing the algorithm SATTdiscussed in Section 2.2. We have also considered the improved PTS T0presented in the last paragraphs of Section 2.2. In this case objects are lists of formulas without complementary elements and the computation rule is defined applying the transformations of ;T0in the order presented in Section