A Certified Polynomial-Based Decision Procedure for Propositional Logic

A Certied Polynomial-Based Decision Pro cedure for Prop ositional Logic Inmaculada Medina-Bulo 1 ,Francisco Palomo-Lozano 1 , and José A. Alonso-Jiménez 2 1 Department of Computer Languages and Systems. University of Cádiz Esc. Sup erior de Ingeniería de Cádiz. C/ Chile, s/n. 11003 Cádiz. Spain {francisco.palomo,inmaculada.medina} @uca .es 2 Department of Comp. Sciences and Articial Intelligence, University of Sevilla Fac. de Informática y Estadística. Avda. Reina Mercedes, s/n. 41012 Sevilla, Spain [email protected] Abstract. In this pap er we present the formalization of a decision procedure for Prop ositional Logic based on p olynomial normalization. This formalization is suitable for its automatic verication in an applicative logic like Acl2 . This application of p olynomials has b een develop ed by reusing a previous work on polynomial rings [19 ], showing that a prop er formalization leads to a high level of reusability. Two checkers are de- ned: the rst for contradiction formulas and the second for tautology formulas. The main theorems state that b oth checkers are sound and complete. Moreover, functions for generating mo dels and counterexamples of formulas are provided. This facility plays also an imp ortant role in the main pro ofs. Finally, it is shown that this allows for a highly automated pro of development. 1Intro duction In this pap er we present the main results obtained through the developmentofan automated proof of the correctness of a polynomial-based decision procedure for Prop ositional Logic in Acl2 [14,15,16]. Acl2 1 is the successor of Nqthm [3,5], the Boyer-Mo ore theorem prover. A concise description of Acl2 can be found in [14]. In order to understand Acl2 , it is necessary to consider it under three dierent p ersp ectives: 1. From a logic viewp oint, Acl2 is a untyp ed quantier-free rst-order logic of total recursive functions with equality.However, its encapsulation principle allows for some kind of higher-order reasoning. 2. From a programming language viewp oint, Acl2 is an applicative programming language in which the result of the application of a function is uniquely determined by its arguments. Every Acl2 function admitted under the definitional principle is a Lisp function, so you can obtain both veried and executable software. 1 A Computational Logic for Applicative Common Lisp. 3. From a reasoning system viewpoint, Acl2 is an automated reasoning system and it b ehaves as a heuristic theorem prover. Representation issues play a ma jor role in this work. We have represented Prop ositional Logic formulas in terms of just one Bo olean function symb ol: the three-place conditional construct present in most programming languages. This is discussed in Sect. 2.1. Denitions related with Bo olean p olynomials are presented in Sect. 2.2. Surprisingly, p olynomial-based theorem proving has a long history.According to H. Zhang [28], Bo ole himself [2] was the rst to use Boolean polynomials to represent logical formulas and Herbrand describ ed a p olynomial-based decision pro cedure in his thesis. Later, in 1936, M. Stone [23] stated the strong relation existing between Bo olean algebras and Bo olean rings. Analogous results had b een discovered, indep endently, in 1927 by I. I. Zhegalkin [29]. This relation is at the basis of the mo dern algebraic methods of logical deduction. The algebraic approach b egan with the development by J. Hsiang of a canonical term-rewriting system for Bo olean algebras with applications to rst-order theorem proving [11,12]. Concurrently,D.Kapur and P. Narendran used Gröbner bases and Buchb erger's algorithm for the same purp ose [17]. 2 This last metho d has b een extended to many-valued propositional logics [7,26] and it has b een recently applied to knowledge based systems verication [18]. Several decision pro cedures for propositional logic that pro duce a veriable pro of log have b een implemented. For example, [9,10] rep ort the developmentof BDDs and Stªmarck's algorithm as HOL derived rules. On the other hand, actual formal verications of decision pro cedures are less common. The classical work from [3] contains a veried decision pro cedure in Nqthm using IF-expressions. A similar pro cedure has b een extracted from a Coq pro of in [22]. Another decision pro cedure obtained via pro of extraction in Nuprl is describ ed in [6]. However, none of them is based on p olynomial normalization. Wehave not considered the p ossibilityofintegrating the decision pro cedure into the theorem prover via reection, though this is feasible in Acl2 thanks to its metatheoretical extensibility capabilities [4]. A reected decision pro cedure has b een develop ed in [1] with Nuprl . See also [8] for a critical survey of reection in theorem proving from a theoretical and practical viewp oint. Section 2.3 presents a translation algorithm from formulas into p olynomials. Once that suitable evaluation functions have b een dened, this translation is shown to b e interpretation-preserving. In Sect. 3, we review Hsiang's canonical term-rewriting system (TRS) for Bo olean algebras. A normalization algorithm that is not based in term-rewriting is also presented. In Sect. 4, we provethe correctness of the decision pro cedure for Prop ositional Logic. As the involved algorithms are written in an applicative subset of Common Lisp , they are intrinsically executable. Some examples of execution are shown in Sect. 5. Finally,we will discuss the degree of automation achieved and we will also analyze some possible extensions of this work. 2 See also [13 ,28 ,27 ]. 2 IF-Formulas and Bo olean Polynomials In [20]an Acl2 formalization of IF-Formulas and Bo olean polynomials is prop osed. Next, the notion of Stone p olynomial of an IF-formula is easily dened. We review here the main results obtained with some improvements. As the conditional construct IF is functionally complete, we can regard our Prop ositional Logic formulas as IF-formulas without loss of generality.In fact, the Nqthm Boyer-Moore logic and its descendant Acl2 dene the usual propositional connectives after axiomatizing IF . IF-formulas are also related with the OBDD algorithm as can be seen in [21]. A BDD manager has b een recently formalized in Acl2 [24]. 2.1 IF-Formulas The underlying representation of IF-formulas is based on the notion of IF-cons. IF-conses are weaker than IF-formulas in the sense that they may not representwell-formed formulas. We use record structures to represent IF-conses. This provides us with a weak recognizer predicate that we strengthen to develop a recognizer for well-formed formulas. Bo olean constants, nil and t , are recognized by the Acl2 booleanp predicate. The set of propositional variables could b e then represented by the set of atoms not including the Bo olean constants. However, if we representvariables using natural numb ers then it is easier to share the same notion of variable in formulas and p olynomials. Thus, we dene our variable recognizer, variablep , to recognize just natural numb ers. Our notion of IF-cons is captured byan Acl2 structure. An IF-cons is just a collection of three ob jects (the test , and the then and else branches). The predicate if-consp will recognize terms constructed with if-cons ,while the functions test , then and else act as destructors. Well-formed IF-formulas can b e recognized by the following total recursive Acl2 predicate: (defun formulap (f) (or (booleanp f) (variablep f) (and (if-consp f) (formulap (test f)) (formulap (then f)) (formulap (else f))))) An assignmentof values to variables can be represented as a list of Booleans. 3 Thus, the value of a variable with respect to an assignment is given by the element which occupies its corresp onding p osition. (defun truth-value (v a) (nth v a)) 3 Remember each Bo olean variable is represented as a natural number. The value of a formula under an assignment is dened recursively by the following function. To make the valuation function total, we assign an arbitrary meaning to non-formulas. (defun value (f a) (cond ((booleanp f) f) ((variablep f) (truth-value f a)) ((if-consp f) (if (value (test f) a) (value (then f) a) (value (else f) a))) (t nil))) ; for completeness The following theorem states a simple but imp ortant prop erty.It says that the value of a formula under an assignment is true if and only if the value of the negation of that formula under the same assignment is false. Why this prop erty is imp ortant will become clear in Sect. 4. (defthm duality (implies (and (formulap f) (assignmentp a)) (iff (equal (value f a) t) (equal (value (if-cons f nil t) a) nil)))) 2.2 Bo olean Polynomials In order to represent p olynomials with Bo olean co ecients, we can use the Bo olean ring given by {0,1},⊕,∧,0,1 where ⊕ is the logical exclusive disjunction (exclusive-or), ∧ is the logical conjunction and 0 and 1 are regarded as truth-values (false and true). In the following denitions, let B={0,1} and ¬ , ∨ stand for logical negation and logical disjunction, resp ectively. Although it suces with a p olynomial Bo olean ring for our current purp oses, where monomials do not need co ecients, wehave implemented monomials with co ecients and terms to reuse part of a previous work on p olynomial rings [19]. Denition 1. ABoolean term on a nite set V={v1,...,v n} of Boolean variables with an ordering relation <V={(vi,v j):1≤i<j≤n} is a nite product of the form: n  i=1 (vi∨¬ai)∀ia i∈B. (1) We obtain a quite simple representation of a Bo olean term on a given set of variables by using the Bo olean sequence a1,...,a n , namely, vi app ears in the term if and only if ai=1 . The main results that wehaveproved in Acl2 on our Bo olean term formalization may b e summed up in the following points: 1. Bo olean terms form a commutative monoid with resp ect to a suitable multiplication operation. 2. Lexicographical ordering on terms is well-founded. As we usually work with Bo olean terms dened on the same set of variables, their sequences will have the same length. In this case they are said to b e compatible . Denition 2. We dene the multiplication of two compatible terms as the following operation: n  i=1 (vi∨¬ai)· n  i=1 (vi∨¬bi)= n  i=1 (vi∨¬(ai∨bi)) . (2) Having chosen the set of variables, it suces to or their sequences element by element to compute the multiplication of two compatible terms. A pro of of terms having a commutative monoid structure with resp ect to the previous op eration is easily obtained. To order terms it is only necessary to take into account their asso ciated sequences. The obvious choice is to set up a lexicographical ordering among them. In the case of compatible terms, this denition is straightforward, since the sequences involved have the same length. Denition 3. The lexicographical ordering on compatible Boolean terms is de- ned as the fol lowing relation: a1,...,a n<b1,...,b n≡∃i(¬ai∧bi∧∀j<ia j=bj). (3) Denition 4. ABoolean monomial on V is the product of a Boolean coecient andaBoolean term. c∧ n  i=1 (vi∨¬ai)c∈B∀ia i∈B. (4) In the same way as happened to terms, it is suitable to dene a compatibility relation on monomials. Wesay that two monomials are compatible when their underlying terms are compatible. Amultiplication op eration is dened and then it is proved that monomials have a monoid commutative structure with resp ect to it. Due to technical reasons it is convenient to extend compatibility of monomials to p olynomials. Toachieve this we rst say that a p olynomial is uniform if all of its monomials are compatible each other. Henceforth, we will assume uniformity. Denition 5. ABoolean polynomial on V is a nite sum of monomials. m  i=1  ci∧ n  j=1 (vj∨¬aij ) ∀i, j ci,a ij ∈B. (5) Now, the denition of compatibilitybetween p olynomials arises in a natural way.Two p olynomials are compatible if their monomials are compatible to o. Finally,wehave proved that Bo olean p olynomials have a ring structure. To achieve this, only co ecients and terms had to b e changed from the formalization describ ed in [19]. These changes are rep orted in [20]. 2.3 Interpretation Preserving Translation Next, we use the relation b etween Boolean rings and Bo olean algebras to derive the translation algorithm. Let us consider a Bo olean algebra and the following three place Bo olean function if , dened on it: ∀a, b, c ∈Bif (a, b, c)=(a∧b)∨(¬a∧c). (6) We can build an asso ciated if function in the corresp onding Bo olean ring: if (a, b, c)=a·b·(a+1)·c+a·b+(a+1)·c=a·b+a·c+c. The following Acl2 functions use this to compute the p olynomial asso ciated to a formula (Stone p olynomial). The function variable->polynomial transforms a prop ositional variable into a suitable p olynomial. The underlying p olynomial Bo olean ring is represented by  polynomialp , + , * , null , identity  . The argument of the function identity isatechnical detail that guarantees the uniformity of the resulting p olynomial. (defun stone (f) (stone-aux f (max-variable f))) (defun stone-aux (f n) (cond ((booleanp f) (if f (identity (LISP::+ n 1)) (null))) ((variablep f) (variable->polynomial f n)) ((if-consp f) (let ((s-test (stone-aux (test f) n)) (s-then (stone-aux (then f) n)) (s-else (stone-aux (else f) n))) (+ (* s-test (+ s-then s-else)) s-else))) (t (null)))) ; for completeness Then, a function, ev ,toevaluate a p olynomial with resp ect to an assignment is dened. Finally,itisproved that the translation of formulas into p olynomials preserves the interpretation: (defthm interpretation-preserving-translatio n (implies (and (formulap f) (assignmentp a)) (iff (value f a) (ev (stone f) a)))) The hard part of the work is dealing with the theorems ab out the evaluation function and p olynomial op erations. 3 Normalization In this section, we review the Hsiang's Canonical TRS and develop a straightforward normalization pro cedure for Bo olean p olynomials. Unlike disjunctive and conjunctive normal forms, p olynomial normalization allows us to associate a unique p olynomial to each Propositional Logic Formula. 3.1 Hsiang's Canonical TRS for Bo olean Algebras A Bo olean ring with identity B,+,·,0,1 isaring that is idemp otent with resp ect to · .Itisaknown fact that every Bo olean ring is nilpotent with respect to + and commutative. Hsiang [11,12] derives his canonical term-rewriting system for Bo olean algebras by rst generating a canonical system for Bo olean rings. Firstly, he considers the Bo olean ring axioms: 4 A1. a+(b+c)=(a+b)+c (asso ciativityof + ). A2. a+b=b+a (commutativityof + ). A3. a+0=a (rightidentityof + ). A4. a+(−a)=0 (rightinverse of + ). A5. (a·b)·c=a·(b·c) (asso ciativityof · ). A6. a·(b+c)=a·b+a·c (distributivityof · over + ). A7. a·1=a (rightidentityof · ). A8. a·a=a (idemp otency of · ). T1. a+a=0 (nilp otency of + ). T2. a·b=b·a (commutativityof · ). By executing the AC-completion pro cedure on these rules, he obtains the BR canonical TRS for Bo olean rings. Then, BR can b e completed 5 by adding rules for transforming the usual Boolean algebraic op erations into Bo olean ring op erations, obtaining the BA canonical TRS for Boolean algebras. BR: BA: a+0−→ a, a·(b+c)−→ a·b+a·c, a·0−→ 0, a·1−→ a, a·a−→ a, a+a−→ 0, −a−→ a. a∨b−→ a·b+a+b, a∧b−→ a·b, ¬a−→ a+1, a=⇒b−→ a·b+a+1, a⇐⇒ b−→ a·b·1, a+0−→ a, a·(b+c)−→ a·b+a·c, a·0−→ 0, a·1−→ a, a·a−→ a, a+a−→ 0. 4 Note that, T1 and T2 are not axioms, but theorems that are added so that the AC-unication algorithm can b e used. 5 The −a−→ a rule is discarded since the inverse of + has no signicant meaning in Bo olean algebras. Therefore, the irreducible form of any Boolean algebra term is the normal expression dened by the BA TRS ab ove, and it is unique (since BA is a canonical TRS). This implies that a formula from Prop ositional Logic is a tautology if and only if its irreducible expression is 1 , and it is a contradiction if and only if its irreducible expression is 0 . 3.2 A Straightforward Normalization Algorithm An algorithm can be develop ed to avoid the overhead asso ciated to Hsiang's TRS. Instead of rewriting mo dulo BA, formulas are translated to p olynomials and then p olynomial normalization is used. Once wehave dened an order on terms, we can say that a p olynomial is in normal form if and only if their monomials are strictly ordered by the decreasing term order and none of them is null. This denition implies the absence of identical monomials in a normalized uniform p olynomial. We divide the sp ecication of the normalization function in two steps: 1. A function capable of adding a monomial to a polynomial. This must b e a normalization-preserving function. 2. A normalization function stable for normalized null polynomials that adds the rst monomial to the normalization of the remaining monomials by using the previous function. The normalization function is easy to dene: if the p olynomial is null, it is already in normal form, otherwise, it suces to normalize the rest of the p olynomial and then add the rst monomial to the result. (defun nf (p) (cond ((or (not (polynomialp p)) (nullp p)) (null)) (t (+-monomial (first p) (nf (rest p)))))) In order to make +-monomial total we need to complete, taking the utmost care, the values that it returns when it is not applied to a p olynomial. Next, we show the most imp ortant part of the denition of +-monomial function. It takes a monomial m and a p olynomial p as its arguments. 1. If m is null, p is returned. 2. If p is null, the p olynomial composed of m is returned. 3. If m and the rst monomial of p have the same term, both monomials are added. If the result is null then the rest of p is returned, otherwise a polynomial consisting of the resulting monomial and the rest of p is returned. 4. If m is greater than the rst monomial of p , a p olynomial consisting of m and p is returned. 5. Otherwise, a p olynomial consisting of the rst monomial of p and the result of recursively adding m to the rest of p is returned. Imp ortant prop erties of the normalization function have been proved, such as that it meets its sp ecication, (defun nfp (p) (equal (nf p) p)) (defthm nfp-nf (nfp (nf p))) and that p olynomial uniformity is preserved under normalization. (defun uniformp (p) (or (nullp p) (nullp (rest p)) (and (MON::compatiblep (first p) (first (rest p))) (uniformp (rest p))))) (defthm uniformp-nf (implies (uniformp p) (uniformp (nf p)))) One relevant result states that the normal form of a polynomial is strictly decreasingly ordered with resp ect to the lexicographical order dened on terms. (defthm orderedp-nf (orderedp (nf p))) In order to obtain this, we dene the function orderedp by using the lexicographical order dened on terms. (defun term-greater-than-leader (m p) (or (nullp p) (TER::< (MON::term (first p)) (MON::term m)))) (defun orderedp (p) (and (polynomialp p) (or (nullp p) (and (not (MON::nullp (first p))) (term-greater-than-leader (first p) (rest p)) (orderedp (rest p)))))) 4 A Decision Pro cedure In this section, our main aim is to construct a p olynomial-based pro cedure for deciding whether a propositional logic formula is a tautology and prove its correctness. A formula is a tautology if and only if the value of the formula under every p ossible assignment of values to variables is true. So, the following rst-order formula states the correctness of a tautology-checker: ∀f[ (tautology-checker f ) ⇐⇒ ∀ a (value fa ) = t ] (7) However, it is not p ossible to write directly this theorem in Acl2 , due to the lackofquantiers. For example, the following theorem do es not capture our idea: 9. Harrison, J.: Binary Decision Diagrams as a HOL Derived Rule. The Computer Journal 38 (1995) 10. Harrison, J.: Stªmarck's Algorithm as a HOL Derived Rule. 9th International Conference on Theorem Proving in Higher Order Logics. LNCS 1125 (1996) 11. Hsiang, J.: Refutational Theorem Proving using Term-Rewriting Systems. Arti- cial Intelligence 25 (1985) 12. Hsiang, J.: Rewrite Metho d for Theorem Proving in First-Order Theory with Equality. J. Symbolic Computation 3 (1987) 13. Hsiang, J., Huang, G. S.: Some Fundamental Prop erties of Bo olean Ring Normal Forms. DIMACS series on Discrete Mathematics and Computer Science: The Satisability Problem. AMS (1996) 14. Kaufmann, M., Mo ore, J S.: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. on Software Engineering 23 (4) (1997) 15. Kaufmann, M., Manolios, P., Mo ore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000) 16. Kaufmann, M., Manolios, P., Mo ore, J S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (2000) 17. Kapur, D., Narendran, P.: An Equational Approach to Theorem Proving in FirstOrder Predicate Calculus. 9th International Conference on Articial Intelligence (1985) 18. Laita, L. M., Roanes-Lozano, E., Ledesma, L., Alonso, J. A.: A Computer Algebra ApproachtoVerication and Deduction in Many-Valued Knowledge Systems. Soft Computing 3 (1) (1999) 19. Medina-Bulo, I., Alonso-Jiménez, J. A., Palomo-Lozano, F.: Automatic Verication of Polynomial Rings Fundamental Properties in ACL2. ACL2 Workshop 2000 Pro ceedings, Part A. The Universityof Texas at Austin, Department of Computer Sciences. Technical Rep ort TR0029 (2000) 20. Medina-Bulo, I., Palomo-Lozano, F., Alonso-Jiménez, J. A.: A Certied Algorithm for Translating Formulas into Polynomials. An ACL2 Approach. International Joint Conference on Automated Reasoning (2001) 21. Mo ore, J S.: Intro duction to the OBDD Algorithm for the ATP Community. Computational Logic, Inc. Technical Rep ort 84 (1992) 22. Paulin-Mohring, C., Werner, B.: Synthesis of ML Programs in the System Co q. J. Symb olic Computation 15 (56) (1993) 23. Stone, M.: The Theory of Representation for Boolean Algebra. Trans. AMS 40 (1936) 24. Sumners, R.: Correctness Pro of of a BDD Manager in the Context of Satisability Checking. ACL2 Workshop 2000 Pro ceedings, Part A. The Universityof Texas at Austin, Department of Computer Sciences. Technical Rep ort TR0029 (2000) 25. Théry,L. AMachine-Checked Implementation of Buchb erger's Algorithm. J. Automated Reasoning 26 (2001) 26. Wu, J., Tan, H.: An Algebraic Metho d to Decide the Deduction Problem in Prop ositional Many-Valued Logics. International Symp osium on Multiple-Valued Logics. IEEE Computer So ciety Press (1994) 27. Wu, J.: First-Order Polynomial Based Theorem Proving. In: Gao, X., Wang, D. (eds.): Mathematics Mechanization and Applications. Academic Press (1999) 28. Zhang, H.: A New Strategy for the Bo olean Ring Based Approach to First Order Theorem Proving. Department of Computer Science. Universityof Iowa. Technical Rep ort (1991) 29. Zhegalkin, I. I.: OnaTechnique of Evaluation of Prop ositions in Symb olic Logic. Mat. Sb. 34 (1927)