A Certified Polynomial-Based Decision Procedure for Propositional Logic

A Ce ied Polynomial-Based Decision P o cedu e o P op osi ional Logic Inmaculada Medina-Bulo 1 ,F ancisco Palomo-Lozano 1 , and José A. Alonso-Jiménez 2 1 Depa men o Compu e Languages and Sys ems. Uni e si y o Cádiz Esc. Sup e io de Ingenie ía de Cádiz. C/ Chile, s/n. 11003 Cádiz. Spain { ancisco.palomo,inmaculada.medina} @uca .es 2 Depa men o Comp. Sciences and A icial In elligence, Uni e si y o Se illa Fac. de In o má ica y Es adís ica. A da. Reina Me cedes, s/n. 41012 Se illa, Spain [email p o ec ed] Abs ac . In his pap e we p esen he o maliza ion o a decision p o- cedu e o P op osi ional Logic based on p olynomial no maliza ion. This o maliza ion is sui able o i s au oma ic e ica ion in an applica i e logic like Acl2 . This applica ion o p olynomials has b een de elop ed by eusing a p e ious wo k on polynomial ings [19 ], showing ha a p op e o maliza ion leads o a high le el o eusabili y. Two checke s a e de- ned: he  s o con adic ion o mulas and he second o au ology o mulas. The main heo ems s a e ha b o h checke s a e sound and comple e. Mo eo e , unc ions o gene a ing mo dels and coun e exam- ples o o mulas a e p o ided. This acili y plays also an imp o an ole in he main p o o s. Finally, i is shown ha his allows o a highly au oma ed p o o de elopmen . 1In o duc ion In his pap e we p esen he main esul s ob ained h ough he de elopmen o an au oma ed p oo o he co ec ness o a polynomial-based decision p ocedu e o P op osi ional Logic in Acl2 [14,15,16]. Acl2 1 is he successo o Nq hm [3,5], he Boye -Mo o e heo em p o e . A concise desc ip ion o Acl2 can be ound in [14]. In o de o unde s and Acl2 , i is necessa y o conside i unde h ee die en p e sp ec i es: 1. F om a logic iewp oin , Acl2 is a un yp ed quan ie - ee  s -o de logic o o al ecu si e unc ions wi h equali y.Howe e , i s encapsula ion p inciple allows o some kind o highe -o de easoning. 2. F om a p og amming language iewp oin , Acl2 is an applica i e p og am- ming language in which he esul o he applica ion o a unc ion is uniquely de e mined by i s a gumen s. E e y Acl2 unc ion admi ed unde he de - ini ional p inciple is a Lisp unc ion, so you can ob ain bo h e ied and execu able so wa e. 1 A Compu a ional Logic o Applica i e Common Lisp. 3. F om a easoning sys em iewpoin , Acl2 is an au oma ed easoning sys em and i b eha es as a heu is ic heo em p o e . Rep esen a ion issues play a ma jo ole in his wo k. We ha e ep esen ed P op osi ional Logic o mulas in e ms o jus one Bo olean unc ion symb ol: he h ee-place condi ional cons uc p esen in mos p og amming languages. This is discussed in Sec . 2.1. Deni ions ela ed wi h Bo olean p olynomials a e p e- sen ed in Sec . 2.2. Su p isingly, p olynomial-based heo em p o ing has a long his o y.Acco ding o H. Zhang [28], Bo ole himsel [2] was he  s o use Boolean polynomials o ep esen logical o mulas and He b and desc ib ed a p olynomial-based decision p o cedu e in his hesis. La e , in 1936, M. S one [23] s a ed he s ong ela ion exis ing be ween Bo olean algeb as and Bo olean ings. Analogous esul s had b een disco e ed, indep enden ly, in 1927 by I. I. Zhegalkin [29]. This ela ion is a he basis o he mo de n algeb aic me hods o logical deduc ion. The algeb aic app oach b egan wi h he de elopmen by J. Hsiang o a canonical e m- ew i ing sys em o Bo olean algeb as wi h applica ions o  s -o de heo em p o ing [11,12]. Concu en ly,D.Kapu and P. Na end an used G öbne bases and Buchb e ge 's algo i hm o he same pu p ose [17]. 2 This las me ho d has b een ex ended o many- alued p oposi ional logics [7,26] and i has b een ecen ly applied o knowledge based sys ems e ica ion [18]. Se e al decision p o cedu es o p oposi ional logic ha p o duce a e iable p o o log ha e b een implemen ed. Fo example, [9,10] ep o he de elopmen o BDDs and S ªma ck's algo i hm as HOL de i ed ules. On he o he hand, ac ual o mal e ica ions o decision p o cedu es a e less common. The classical wo k om [3] con ains a e ied decision p o cedu e in Nq hm using IF-exp essions. A simila p o cedu e has b een ex ac ed om a Coq p o o in [22]. Ano he decision p o cedu e ob ained ia p o o ex ac ion in Nup l is desc ib ed in [6]. Howe e , none o hem is based on p olynomial no maliza ion. Weha e no conside ed he p ossibili yo in eg a ing he decision p o cedu e in o he heo em p o e ia eec ion, hough his is easible in Acl2 hanks o i s me a heo e ical ex ensibili y capabili ies [4]. A eec ed decision p o ce- du e has b een de elop ed in [1] wi h Nup l . See also [8] o a c i ical su ey o eec ion in heo em p o ing om a heo e ical and p ac ical iewp oin . Sec ion 2.3 p esen s a ansla ion algo i hm om o mulas in o p olynomials. Once ha sui able e alua ion unc ions ha e b een dened, his ansla ion is shown o b e in e p e a ion-p ese ing. In Sec . 3, we e iew Hsiang's canonical e m- ew i ing sys em (TRS) o Bo olean algeb as. A no maliza ion algo i hm ha is no based in e m- ew i ing is also p esen ed. In Sec . 4, we p o e he co ec ness o he decision p o cedu e o P op osi ional Logic. As he in ol ed algo i hms a e w i en in an applica i e subse o Common Lisp , hey a e in- insically execu able. Some examples o execu ion a e shown in Sec . 5. Finally,we will discuss he deg ee o au oma ion achie ed and we will also analyze some possible ex ensions o his wo k. 2 See also [13 ,28 ,27 ]. 2 IF-Fo mulas and Bo olean Polynomials In [20]an Acl2 o maliza ion o IF-Fo mulas and Bo olean polynomials is p o- p osed. Nex , he no ion o S one p olynomial o an IF- o mula is easily dened. We e iew he e he main esul s ob ained wi h some imp o emen s. As he condi ional cons uc IF is unc ionally comple e, we can ega d ou P op osi ional Logic o mulas as IF- o mulas wi hou loss o gene ali y.In ac , he Nq hm Boye -Moo e logic and i s descendan Acl2 dene he usual p opo- si ional connec i es a e axioma izing IF . IF- o mulas a e also ela ed wi h he OBDD algo i hm as can be seen in [21]. A BDD manage has b een ecen ly o malized in Acl2 [24]. 2.1 IF-Fo mulas The unde lying ep esen a ion o IF- o mulas is based on he no ion o IF-cons. IF-conses a e weake han IF- o mulas in he sense ha hey may no ep e- sen well- o med o mulas. We use eco d s uc u es o ep esen IF-conses. This p o ides us wi h a weak ecognize p edica e ha we s eng hen o de elop a ecognize o well- o med o mulas. Bo olean cons an s, nil and , a e ecognized by he Acl2 booleanp p edi- ca e. The se o p oposi ional a iables could b e hen ep esen ed by he se o a oms no including he Bo olean cons an s. Howe e , i we ep esen a iables using na u al numb e s hen i is easie o sha e he same no ion o a iable in o mulas and p olynomials. Thus, we dene ou a iable ecognize , a iablep , o ecognize jus na u al numb e s. Ou no ion o IF-cons is cap u ed byan Acl2 s uc u e. An IF-cons is jus a collec ion o h ee ob jec s ( he es , and he hen and else b anches). The p edica e i -consp will ecognize e ms cons uc ed wi h i -cons ,while he unc ions es , hen and else ac as des uc o s. Well- o med IF- o mulas can b e ecognized by he ollowing o al ecu si e Acl2 p edica e: (de un o mulap ( ) (o (booleanp ) ( a iablep ) (and (i -consp ) ( o mulap ( es )) ( o mulap ( hen )) ( o mulap (else ))))) An assignmen o alues o a iables can be ep esen ed as a lis o Booleans. 3 Thus, he alue o a a iable wi h espec o an assignmen is gi en by he elemen which occupies i s co esp onding p osi ion. (de un u h- alue ( a) (n h a)) 3 Remembe each Bo olean a iable is ep esen ed as a na u al numbe . The alue o a o mula unde an assignmen is dened ecu si ely by he ollowing unc ion. To make he alua ion unc ion o al, we assign an a bi a y meaning o non- o mulas. (de un alue ( a) (cond ((booleanp ) ) (( a iablep ) ( u h- alue a)) ((i -consp ) (i ( alue ( es ) a) ( alue ( hen ) a) ( alue (else ) a))) ( nil))) ; o comple eness The ollowing heo em s a es a simple bu imp o an p op e y.I says ha he alue o a o mula unde an assignmen is ue i and only i he alue o he nega ion o ha o mula unde he same assignmen is alse. Why his p op e y is imp o an will become clea in Sec . 4. (de hm duali y (implies (and ( o mulap ) (assignmen p a)) (i (equal ( alue a) ) (equal ( alue (i -cons nil ) a) nil)))) 2.2 Bo olean Polynomials In o de o ep esen p olynomials wi h Bo olean co ecien s, we can use he Bo olean ing gi en by {0,1},⊕,∧,0,1 whe e ⊕ is he logical exclusi e dis- junc ion (exclusi e-o ), ∧ is he logical conjunc ion and 0 and 1 a e ega ded as u h- alues ( alse and ue). In he ollowing deni ions, le B={0,1} and ¬ , ∨ s and o logical nega ion and logical disjunc ion, esp ec i ely. Al hough i suces wi h a p olynomial Bo olean ing o ou cu en pu p oses, whe e monomials do no need co ecien s, weha e implemen ed monomials wi h co ecien s and e ms o euse pa o a p e ious wo k on p olynomial ings [19]. Deni ion 1. ABoolean e m on a ni e se V={ 1,..., n} o Boolean a i- ables wi h an o de ing ela ion <V={( i, j):1≤i<j≤n} is a ni e p oduc o he o m: n  i=1 ( i∨¬ai)∀ia i∈B. (1) We ob ain a qui e simple ep esen a ion o a Bo olean e m on a gi en se o a iables by using he Bo olean sequence a1,...,a n , namely, i app ea s in he e m i and only i ai=1 . The main esul s ha weha ep o ed in Acl2 on ou Bo olean e m o maliza ion may b e summed up in he ollowing poin s: 1. Bo olean e ms o m a commu a i e monoid wi h esp ec o a sui able mul- iplica ion ope a ion. 2. Lexicog aphical o de ing on e ms is well- ounded. As we usually wo k wi h Bo olean e ms dened on he same se o a i- ables, hei sequences will ha e he same leng h. In his case hey a e said o b e compa ible . Deni ion 2. We dene he mul iplica ion o wo compa ible e ms as he ol- lowing ope a ion: n  i=1 ( i∨¬ai)· n  i=1 ( i∨¬bi)= n  i=1 ( i∨¬(ai∨bi)) . (2) Ha ing chosen he se o a iables, i suces o o  hei sequences elemen by elemen o compu e he mul iplica ion o wo compa ible e ms. A p o o o e ms ha ing a commu a i e monoid s uc u e wi h esp ec o he p e ious op e a ion is easily ob ained. To o de e ms i is only necessa y o ake in o accoun hei asso cia ed sequences. The ob ious choice is o se up a lexicog aphical o de ing among hem. In he case o compa ible e ms, his deni ion is s aigh o wa d, since he sequences in ol ed ha e he same leng h. Deni ion 3. The lexicog aphical o de ing on compa ible Boolean e ms is de- ned as he ol lowing ela ion: a1,...,a n<b1,...,b n≡∃i(¬ai∧bi∧∀j<ia j=bj). (3) Deni ion 4. ABoolean monomial on V is he p oduc o a Boolean coecien andaBoolean e m. c∧ n  i=1 ( i∨¬ai)c∈B∀ia i∈B. (4) In he same way as happened o e ms, i is sui able o dene a compa ibili y ela ion on monomials. Wesay ha wo monomials a e compa ible when hei unde lying e ms a e compa ible. Amul iplica ion op e a ion is dened and hen i is p o ed ha monomials ha e a monoid commu a i e s uc u e wi h esp ec o i . Due o echnical easons i is con enien o ex end compa ibili y o monomials o p olynomials. Toachie e his we  s say ha a p olynomial is uni o m i all o i s monomials a e compa ible each o he . Hence o h, we will assume uni o mi y. Deni ion 5. ABoolean polynomial on V is a ni e sum o monomials. m  i=1  ci∧ n  j=1 ( j∨¬aij ) ∀i, j ci,a ij ∈B. (5) Now, he deni ion o compa ibili ybe ween p olynomials a ises in a na u al way.Two p olynomials a e compa ible i hei monomials a e compa ible o o. Finally,weha e p o ed ha Bo olean p olynomials ha e a ing s uc u e. To achie e his, only co ecien s and e ms had o b e changed om he o maliza ion desc ib ed in [19]. These changes a e ep o ed in [20]. 2.3 In e p e a ion P ese ing T ansla ion Nex , we use he ela ion b e ween Boolean ings and Bo olean algeb as o de i e he ansla ion algo i hm. Le us conside a Bo olean algeb a and he ollowing h ee place Bo olean unc ion i , dened on i : ∀a, b, c ∈Bi (a, b, c)=(a∧b)∨(¬a∧c). (6) We can build an asso cia ed i unc ion in he co esp onding Bo olean ing: i (a, b, c)=a·b·(a+1)·c+a·b+(a+1)·c=a·b+a·c+c. The ollowing Acl2 unc ions use his o compu e he p olynomial asso ci- a ed o a o mula (S one p olynomial). The unc ion a iable->polynomial ans o ms a p op osi ional a iable in o a sui able p olynomial. The unde lying p olynomial Bo olean ing is ep esen ed by  polynomialp , + , * , null , iden i y  . The a gumen o he unc ion iden i y isa echnical de ail ha gua an ees he uni o mi y o he esul ing p olynomial. (de un s one ( ) (s one-aux (max- a iable ))) (de un s one-aux ( n) (cond ((booleanp ) (i (iden i y (LISP::+ n 1)) (null))) (( a iablep ) ( a iable->polynomial n)) ((i -consp ) (le ((s- es (s one-aux ( es ) n)) (s- hen (s one-aux ( hen ) n)) (s-else (s one-aux (else ) n))) (+ (* s- es (+ s- hen s-else)) s-else))) ( (null)))) ; o comple eness Then, a unc ion, e , oe alua e a p olynomial wi h esp ec o an assignmen is dened. Finally,i isp o ed ha he ansla ion o o mulas in o p olynomials p ese es he in e p e a ion: (de hm in e p e a ion-p ese ing- ansla io n (implies (and ( o mulap ) (assignmen p a)) (i ( alue a) (e (s one ) a)))) The ha d pa o he wo k is dealing wi h he heo ems ab ou he e alua ion unc ion and p olynomial op e a ions. 3 No maliza ion In his sec ion, we e iew he Hsiang's Canonical TRS and de elop a s aigh - o wa d no maliza ion p o cedu e o Bo olean p olynomials. Unlike disjunc i e and conjunc i e no mal o ms, p olynomial no maliza ion allows us o associa e a unique p olynomial o each P oposi ional Logic Fo mula. 3.1 Hsiang's Canonical TRS o Bo olean Algeb as A Bo olean ing wi h iden i y B,+,·,0,1 isa ing ha is idemp o en wi h esp ec o · .I isaknown ac ha e e y Bo olean ing is nilpo en wi h espec o + and commu a i e. Hsiang [11,12] de i es his canonical e m- ew i ing sys em o Bo olean algeb as by  s gene a ing a canonical sys em o Bo olean ings. Fi s ly, he conside s he Bo olean ing axioms: 4 A1. a+(b+c)=(a+b)+c (asso cia i i yo + ). A2. a+b=b+a (commu a i i yo + ). A3. a+0=a ( igh iden i yo + ). A4. a+(−a)=0 ( igh in e se o + ). A5. (a·b)·c=a·(b·c) (asso cia i i yo · ). A6. a·(b+c)=a·b+a·c (dis ibu i i yo · o e + ). A7. a·1=a ( igh iden i yo · ). A8. a·a=a (idemp o ency o · ). T1. a+a=0 (nilp o ency o + ). T2. a·b=b·a (commu a i i yo · ). By execu ing he AC-comple ion p o cedu e on hese ules, he ob ains he BR canonical TRS o Bo olean ings. Then, BR can b e comple ed 5 by adding ules o ans o ming he usual Boolean algeb aic op e a ions in o Bo olean ing op e a ions, ob aining he BA canonical TRS o Boolean algeb as. 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 No e ha , T1 and T2 a e no axioms, bu heo ems ha a e added so ha he AC-unica ion algo i hm can b e used. 5 The −a−→ a ule is disca ded since he in e se o + has no signican meaning in Bo olean algeb as. The e o e, he i educible o m o any Boolean algeb a e m is he no mal exp ession dened by he BA TRS ab o e, and i is unique (since BA is a canonical TRS). This implies ha a o mula om P op osi ional Logic is a au ology i and only i i s i educible exp ession is 1 , and i is a con adic ion i and only i i s i educible exp ession is 0 . 3.2 A S aigh o wa d No maliza ion Algo i hm An algo i hm can be de elop ed o a oid he o e head asso cia ed o Hsiang's TRS. Ins ead o ew i ing mo dulo BA, o mulas a e ansla ed o p olynomials and hen p olynomial no maliza ion is used. Once weha e dened an o de on e ms, we can say ha a p olynomial is in no mal o m i and only i hei monomials a e s ic ly o de ed by he dec easing e m o de and none o hem is null. This deni ion implies he absence o iden ical monomials in a no malized uni o m p olynomial. We di ide he sp ecica ion o he no maliza ion unc ion in wo s eps: 1. A unc ion capable o adding a monomial o a polynomial. This mus b e a no maliza ion-p ese ing unc ion. 2. A no maliza ion unc ion s able o no malized null polynomials ha adds he  s monomial o he no maliza ion o he emaining monomials by using he p e ious unc ion. The no maliza ion unc ion is easy o dene: i he p olynomial is null, i is al eady in no mal o m, o he wise, i suces o no malize he es o he p olynomial and hen add he  s monomial o he esul . (de un n (p) (cond ((o (no (polynomialp p)) (nullp p)) (null)) ( (+-monomial ( i s p) (n ( es p)))))) In o de o make +-monomial o al we need o comple e, aking he u mos ca e, he alues ha i e u ns when i is no applied o a p olynomial. Nex , we show he mos imp o an pa o he deni ion o +-monomial unc ion. I akes a monomial m and a p olynomial p as i s a gumen s. 1. I m is null, p is e u ned. 2. I p is null, he p olynomial composed o m is e u ned. 3. I m and he  s monomial o p ha e he same e m, bo h monomials a e added. I he esul is null hen he es o p is e u ned, o he wise a poly- nomial consis ing o he esul ing monomial and he es o p is e u ned. 4. I m is g ea e han he  s monomial o p , a p olynomial consis ing o m and p is e u ned. 5. O he wise, a p olynomial consis ing o he  s monomial o p and he esul o ecu si ely adding m o he es o p is e u ned. Imp o an p op e ies o he no maliza ion unc ion ha e been p o ed, such as ha i mee s i s sp ecica ion, (de un n p (p) (equal (n p) p)) (de hm n p-n (n p (n p))) and ha p olynomial uni o mi y is p ese ed unde no maliza ion. (de un uni o mp (p) (o (nullp p) (nullp ( es p)) (and (MON::compa iblep ( i s p) ( i s ( es p))) (uni o mp ( es p))))) (de hm uni o mp-n (implies (uni o mp p) (uni o mp (n p)))) One ele an esul s a es ha he no mal o m o a polynomial is s ic ly dec easingly o de ed wi h esp ec o he lexicog aphical o de dened on e ms. (de hm o de edp-n (o de edp (n p))) In o de o ob ain his, we dene he unc ion o de edp by using he lexico- g aphical o de dened on e ms. (de un e m-g ea e - han-leade (m p) (o (nullp p) (TER::< (MON:: e m ( i s p)) (MON:: e m m)))) (de un o de edp (p) (and (polynomialp p) (o (nullp p) (and (no (MON::nullp ( i s p))) ( e m-g ea e - han-leade ( i s p) ( es p)) (o de edp ( es p)))))) 4 A Decision P o cedu e In his sec ion, ou main aim is o cons uc a p olynomial-based p o cedu e o deciding whe he a p oposi ional logic o mula is a au ology and p o e i s co - ec ness. A o mula is a au ology i and only i he alue o he o mula unde e e y p ossible assignmen o alues o a iables is ue. So, he ollowing  s -o de o mula s a es he co ec ness o a au ology-checke : ∀ [ ( au ology-checke ) ⇐⇒ ∀ a ( alue a ) = ] (7) Howe e , i is no p ossible o w i e di ec ly his heo em in Acl2 , due o he lacko quan ie s. Fo example, he ollowing  heo em do es no cap u e ou idea: 9. Ha ison, J.: Bina y Decision Diag ams as a HOL De i ed Rule. The Compu e Jou nal 38 (1995) 10. Ha ison, J.: S ªma ck's Algo i hm as a HOL De i ed Rule. 9 h In e na ional Con e ence on Theo em P o ing in Highe O de Logics. LNCS 1125 (1996) 11. Hsiang, J.: Re u a ional Theo em P o ing using Te m-Rew i ing Sys ems. A i- cial In elligence 25 (1985) 12. Hsiang, J.: Rew i e Me ho d o Theo em P o ing in Fi s -O de Theo y wi h Equali y. J. Symbolic Compu a ion 3 (1987) 13. Hsiang, J., Huang, G. S.: Some Fundamen al P op e ies o Bo olean Ring No mal Fo ms. DIMACS se ies on Disc e e Ma hema ics and Compu e Science: The Sa isabili y P oblem. AMS (1996) 14. Kau mann, M., Mo o e, J S.: An Indus ial S eng h Theo em P o e o a Logic Based on Common Lisp. IEEE T ans. on So wa e Enginee ing 23 (4) (1997) 15. Kau mann, M., Manolios, P., Mo o e, J S.: Compu e -Aided Reasoning: An Ap- p oach. Kluwe Academic Publishe s (2000) 16. Kau mann, M., Manolios, P., Mo o e, J S.: Compu e -Aided Reasoning: ACL2 Case S udies. Kluwe Academic Publishe s (2000) 17. Kapu , D., Na end an, P.: An Equa ional App oach o Theo em P o ing in Fi s - O de P edica e Calculus. 9 h In e na ional Con e ence on A icial In elligence (1985) 18. Lai a, L. M., Roanes-Lozano, E., Ledesma, L., Alonso, J. A.: A Compu e Algeb a App oach oVe ica ion and Deduc ion in Many-Valued Knowledge Sys ems. So Compu ing 3 (1) (1999) 19. Medina-Bulo, I., Alonso-Jiménez, J. A., Palomo-Lozano, F.: Au oma ic Ve ica ion o Polynomial Rings Fundamen al P ope ies in ACL2. ACL2 Wo kshop 2000 P o ceedings, Pa A. The Uni e si yo Texas a Aus in, Depa men o Compu e Sciences. Technical Rep o TR0029 (2000) 20. Medina-Bulo, I., Palomo-Lozano, F., Alonso-Jiménez, J. A.: A Ce ied Algo i hm o T ansla ing Fo mulas in o Polynomials. An ACL2 App oach. In e na ional Join Con e ence on Au oma ed Reasoning (2001) 21. Mo o e, J S.: In o duc ion o he OBDD Algo i hm o he ATP Communi y. Compu a ional Logic, Inc. Technical Rep o 84 (1992) 22. Paulin-Moh ing, C., We ne , B.: Syn hesis o ML P og ams in he Sys em Co q. J. Symb olic Compu a ion 15 (56) (1993) 23. S one, M.: The Theo y o Rep esen a ion o Boolean Algeb a. T ans. AMS 40 (1936) 24. Sumne s, R.: Co ec ness P o o o a BDD Manage in he Con ex o Sa isabili y Checking. ACL2 Wo kshop 2000 P o ceedings, Pa A. The Uni e si yo Texas a Aus in, Depa men o Compu e Sciences. Technical Rep o TR0029 (2000) 25. Thé y,L. AMachine-Checked Implemen a ion o Buchb e ge 's Algo i hm. J. Au- oma ed Reasoning 26 (2001) 26. Wu, J., Tan, H.: An Algeb aic Me ho d o Decide he Deduc ion P oblem in P op o- si ional Many-Valued Logics. In e na ional Symp osium on Mul iple-Valued Logics. IEEE Compu e So cie y P ess (1994) 27. Wu, J.: Fi s -O de Polynomial Based Theo em P o ing. In: Gao, X., Wang, D. (eds.): Ma hema ics Mechaniza ion and Applica ions. Academic P ess (1999) 28. Zhang, H.: A New S a egy o he Bo olean Ring Based App oach o Fi s O de Theo em P o ing. Depa men o Compu e Science. Uni e si yo Iowa. Technical Rep o (1991) 29. Zhegalkin, I. I.: OnaTechnique o E alua ion o P op osi ions in Symb olic Logic. Ma . Sb. 34 (1927)