Formal verification of a generic framework to synthesize SAT-provers

Fo mal e i ica ion o a gene ic amewo k o syn hesize SAT-p o e s F ancisco–Jes´us Ma ´ın–Ma eos, Jos´e–An onio Alonso, Ma ´ıa–Jose´ Hidalgo and Jos´e–Luis Ruiz–Reina Compu a ional Logic G oup Dep . o Compu e Science and A i icial In elligence, Uni e si y o Se ille E.T.S.I. In o m´a ica, A da. Reina Me cedes, s/n. 41012 Se illa, Spain E-mails: { ma in,jalonso,mjoseh,j uiz}@cs.us.es Abs ac . We p esen in his pape an applica ion o he ACL2 sys em o gene a e and eason abou p oposi ional sa is iabili y p o e s. Fo ha pu pose, we de elop a amewo k whe e we de ine a gene ic SAT-p o e based on ans o ma ion ules, and we o malize his gene ic amewo k in he ACL2 logic, ca ying ou a o mal p oo o i s e mina ion, soundness and comple eness. This gene ic amewo k can be ins an ia ed o ob ain a numbe o e i ied and execu able SAT-p o e s in ACL2, and his can be done in an au oma ed way. Th ee ins an ia ions o he gene ic amewo k a e conside ed: seman ic ableaux, sequen and Da is–Pu nam–Logeman–Lo eland me hods. 1. In oduc ion A common p ac ice in p og am e i ica ion is s epwise e inemen . This means ha essen ial p ope ies o p og ams can be i s p o ed a a e y abs ac le el, conside ing only a gene ic speci ica ion o he p og am, skipping echnical de ails o conc e e implemen a ions. Thus, he p ope ies p o ed can be deduced o a gi en implemen a ion o he gene ic speci ica ion, by simply showing ha his implemen a ion is a conc e e ins ance o he gene ic p ocedu e. Fu he e inemen s o he implemen a ions (in o de o ob ain be e pe o mance) can s ill be e i ied by showing ha hey compu e he same esul s as an-o he e i ied implemen a ion. In his pape , we desc ibe an applica ion o his echnique o eason o mally abou a amily o p oposi ional sa is iabili y (SAT) decision p ocedu es, using he ACL2 sys em. SAT p o e s a e an impo an componen o many applica ions in heo em p o ing in pa icula and a i icial in elligence in gene al [9], so i makes sense he de elopmen o o mally e i ied SAT decision p ocedu es, as a way o ce i ying his “p oo engine” componen [18]. The eason why we ha e chosen ACL2 as he logic and p o e used o eason abou his p ocedu es, is ha his sys em p o ides a amewo k ∗ This wo k has been suppo ed by p ojec TIC2000-1368-C03-02 (Minis y o Science and Technology, Spain), co inancied by FEDER ounds. 2 whe e easoning and compu ing can be done. ACL2 [12] is a p og am- ming language, a logic o easoning abou p og ams in he language, and a heo em p o e suppo ing o mal easoning in he logic. So he p ocedu es can be implemen ed, execu ed and o mally e i ied in he same sys em. Th ee case s udies a e conside ed: seman ic ableaux, sequen calcu- lus and he Da is–Pu nam–Logeman–Lo eland me hod. The common pa e n o all hese SAT p ocedu es is ha hey can be desc ibed as ule based ans o ma ion sys ems. Fo ha pu pose, we de elop a gene ic amewo k in o which hese SAT-p o e s can be placed. A gene ic SAT- p o e is o malized in ACL2 and i s main p ope ies a e p o ed; using unc ional ins an ia ion, conc e e ins ances o he gene ic amewo k can be de ined o ob ain o mally e i ied and Common Lisp execu able SAT-p o e s. As a byp oduc , we ha e de eloped a ool o make he in- s an ia ion p ocess mo e con enien , ob aining in an au oma ed way he conc e e and execu able p ocedu es and he ins ances o he heo ems p o ed o he gene ic amewo k. This pape is an ex ended and e ised e sion o [15]. I is o ganized as ollows. In Sec ion 2 we de ine a gene ic amewo k in o de o build a gene ic ans o ma ion based SAT-p o e , and we ske ch a p oo o i s e mina ion, soundness and comple eness p ope ies. We also desc ibe how h ee well-known SAT-p o e s me hods ( ableaux, sequen cal- culus and Da is–Pu nam–Logeman–Lo eland me hod) can be placed in o he gene ic amewo k. In Sec ion 3 we show how his amewo k has been o malized in ACL2 and how i s main p ope ies has been p o ed. In Sec ion 4 we desc ibe how hese gene ic de ini ions and he- o ems has been ins an ia ed, o ob ain e i ied and execu able Common Lisp de ini ions o ableaux based, sequen based and Da is–Pu nam– Logeman–Lo eland SAT-p o e s. Finally, in Sec ion 5 we d aw some conclusions. Due o he lack o space we will skip de ails o he mechanical p oo s and o he same eason some unc ion de ini ions will be omi ed. The comple e o maliza ion is a ailable in [16]. 2. A gene ic amewo k o de elop p oposi ional SAT-p o e s Analyzing some well-known me hods o p o ing p oposi ional sa - is iabili y (such as sequen , ableaux o Da is–Pu nam–Logeman– Lo eland), we can obse e a common beha io . They do no wo k di ec ly on o mulas bu on objec s buil om o mulas. The objec s a e epea edly modi ied using expansion ules, educing hei complexi y 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 Figu e 1. An example o ableaux me hod in such a way ha hei meaning is p ese ed. E en ually, om some kind o simple objec s, a dis inguished alua ion p o ing sa is iabili y o he o iginal o mula can be ob ained. I no such objec is ound, hen unsa is iabili y o he o iginal o mula is p o ed. We mus poin ou ha hese objec s a e no only heo e ical s uc u es used o desc ibe he me hod (e.g. lis s o se s o o mulas), bu hey can be eal da a s uc u es used in he implemen a ion (e.g. a ays, linked lis s, hash ables, ...) o he SAT p ocedu es. We can see his beha io in he seman ic ableaux me hod, by means o he example shown in Figu e 1. F om he o mula (p→q)∧p he ini ial ee T1wi h a single node is buil . In a i s s ep he o mula is expanded ob aining one ex ension wi h wo o mulas p→qand p ( ee T2). In a second s ep he o mula p→qis expanded ob aining wo ex ensions, he i s wi h he o mula ¬pand he second wi h he o mula q( ee T3). The le b anch becomes closed (i.e., wi h complemen a y li e als) and he igh one p o ides a model σ. Thus, he ableaux me hod can be seen as he applica ion o a se o expansion ules ac ing on b anches o ees ( he objec s) un il a b anch wi hou complemen a y li e als is ob ained. Fo his b anch, a dis inguished alua ion (making ha b anch ue) is easily ob ained. O he wise, all b anches a e closed and unsa is iabili y is p o ed. Ou goal in his sec ion is o desc ibe a gene ic amewo k whe e hese me hods can be i . Fi s we in oduce some no a ion. We conside an in ini e se o p oposi ion symbols Σ and a se o u h alues, B= { , }, whe e deno es ue and deno es alse.P(Σ) deno es he se o p oposi ional o mulas on Σ ( he u h alues a e no conside ed as o mulas), whe e he basic connec i es a e ¬,∧,∨,→and ↔. The complemen o a o mula F, deno ed as F, is de ined such ha F=G i F=¬G, and F=¬Fo he wise. A li e al is a o mula po ¬p, whe e p∈Σ. A clause is a ini e sequence o li e als. A alua ion is a unc ion 4 σ: Σ −→ B; we deno e VΣ he se o all alua ions de ined on Σ. The alua ions a e ex ended o P(Σ) in he usual way. We deno e σ|=F when σ(F) = , and we say ha σis a model o F. A alua ion σis a model o a clause C, i i is a model o some li e al in C. The capi al G eek le e s Γ and ∆ (possibly wi h subsc ip s) deno e ini e sequences o o mulas (we some imes use he e m lis ins ead o ini e sequence). We will use he no a ion he1, ..., eki o ep esen a ini e sequence, and O∗ o deno e he se o ini e sequences o elemen s o he se O. We say ha xis a membe o he lis he1, ..., eki, deno ed as x∈ he1, ..., eki, i ∃i, 1≤i≤n, such ha x=ei. We w i e hΓ1, F, Γ2io Γ1, F, Γ2, o dis inguish he o mula Fin a sequence o o mulas. Finally, O d deno es he class o all o dinals. 2.1. A gene ic algo i hm o p o ing p oposi ional sa is iabili y DEFINITION 1. AP oposi ional T ans o ma ion Sys em (PTS, o sho ) is a iple G=hOG,;G,|=Gi, whe e OGis a se , and ;Gand |=Ga e bina y ela ions such ha ;G⊆ O×(O∗∪{ })and |=G⊆VΣ×O. We will call OG he se o p oposi ional objec s (o simply objec s) and ;G he se o expansion ules. In ui i ely, he objec s a e he s uc u es used by a p oposi ional SAT-p o e and he expansion ules desc ibe he s eps ha i pe o ms. No e ha we allow ules o he o m O;Ghi and ules o he o m O;G . The i s one ep esen s dead ends in he sea ch o sa is iabili y, and he second one ep esen s success ul ends. When σ|=GO, we say ha σis a dis inguished alua ion o O. The idea is ha when a success ul end is ound, he dis inguished alua ions o he las objec p o ide a model o he o iginal o mula. In ui i ely, he ela ion |=G ansla es he ela ion |= om o mulas o he objec s used by he SAT-p o e . DEFINITION 2. Gi en a PTS G=hOG,;G,|=Gi: 1. A compu a ion ule is a unc ion :O −→ O∗∪ { }such ha ⊆;G. 2. A ep esen a ion unc ion is a unc ion i:P(Σ) −→ O. 3. A measu e unc ion is a unc ion µ:O −→ O d. 4. A model unc ion is a unc ion γ:O −→VΣ, whe e O ={O∈ O : O;G }. 5 Gi en a PTS G=hOG,;G,|=Gi, a compu a ion ule and a ep e- sen a ion unc ion i, we de ine he ollowing algo i hm SATG o p o ing sa is iabili y o a p oposi ional o mula. ALGORITHM 1 (SATG). The inpu o his algo i hm is a p oposi- ional o mula Fand i p oceeds as ollows: 1. Le L=hi(F)i. 2. While Lis a non-emp y lis , do: Selec Oja membe o he lis L=hO1, ..., Oni. a) I (Oj) = , hen s op and e u n hOji. b) I (Oj) = hO0 1, ..., O0 mi(m≥0), hen le L=hO0 1, ..., O0 m, O1, ..., Oj−1, Oj+1, ..., Oni. 3. Re u n . The in ui i e idea is simple: gi en F, we s a wi h he ini ial objec i(F) and epea edly apply he expansion ules un il is ob ained o un il he e a e no mo e objec s le . Te mina ion o his p ocess will be gua an eed by a measu e unc ion µ. The s a egy o apply he ules is de e mined by he gi en compu a ion ule and by he selec ion s a egy o objec s o he lis L. No e ha assuming he exis ence o a compu a ion ule means ha o e e y objec he e is a leas one ule ha can be applied o i . I can be p o ed ha unde some condi ions ha we gi e below, i is ob ained om an objec Oj, hen we can ob ain a dis inguished alua ion using a model unc ion and his alua ion u ns ou o be a model o he o iginal o mula. Unde he same condi ions, i is ob ained, he o iginal o mula is unsa is iable. DEFINITION 3. We say ha SATGis comple e i o all F∈P(Σ) such ha ∃σ∈VΣ:σ|=F, hen SATG(F)6= . We say ha i is sound i o all F∈P(Σ) such ha SATG(F)6= , hen ∃σ∈VΣ:σ|=F. THEOREM 1. Le G=hOG,;G,|=Gibe a PTS, a compu a ion ule, ia ep esen a ion unc ion, µa measu e unc ion and γa model unc ion, such ha he ollowing p ope ies hold: P1:Oi∈ (O) =⇒µ(Oi)< µ(O) P2:F∈P(Σ) =⇒(σ|=F⇐⇒ σ|=Gi(F)) P3:O∈ O ∧ (O)6= =⇒(σ|=GO⇐⇒ ∃Oi∈ (O), σ |=GOi) 6 P4:O∈ O ∧ (O) = =⇒γ(O)|=GO hen he algo i hm SATG e mina es o any o mula and is comple e and sound. Fu he mo e, i SATG(F) = hOi hen γ(O)|=F. Te mina ion P oo . In he e mina ion p oo o SATG, we will use a mul ise ela ion buil om he measu e unc ion. Roughly speaking, a ini e mul ise o e Ais a subse o A“wi h epea ed elemen s”. Le us b ie ly ecall he no ion o mul ise ela ion. Gi en a ela ion <on a se A, we de ine he mul ise ela ion induced by <on he se o ini e mul ise s o e A, deno ed as <mul, in he ollowing way: N <mul M i he e exis X, Y ini e mul ise s o e A, such ha Ø 6=X⊆M, N= (M X)∪Yand o all y∈Y he e exis s x∈Xsuch ha y < x. In ui i ely, his means ha a smalle mul ise can be ob ained by emo ing a non-emp y subse o elemen s, and adding elemen s which a e smalle han some elemen emo ed. In [7] i is p o ed ha <mul is well- ounded whene e <is well- ounded. Le us now p o e he e mina ion o SATG. Fo ha pu pose, we mus p o e ha poin 2 is a ini e loop. Assume ha he lis o objec s in poin 2 is hO1, ..., Oni, he selec ed elemen is Ojand (Oj) = hO0 1, ..., O0 mi, wi h m≥0. We conside he ela ion <µin Ode ined as ollows O1<µO2i and only i µ(O1)< µ(O2). Ob iously, <µis a well ounded ela ion on O. Then, o e e y k,O0 k<µOjby P1. The e o e, he mul ise {O0 1, ..., O0 m, O1, ..., Oj−1, Oj+1, ..., On}is smalle han {O1, ..., On}wi h espec o he mul ise ex ension o <µ(which is also well- ounded). This p o es e mina ion o SATG. Comple eness P oo . Fi s o all no e ha , by P3, i he algo i hm eaches poin 2-(b), σis a dis inguished alua ion o some objec in he lis conside ed in poin 2 i and only i i is a dis inguished alua ion o some objec in he new lis buil in poin 2-(b). I σ|=F hen, by P2,σ|=Gi(F). Then, by he abo e obse a ion, in e e y lis conside ed in poin 2 exis s Osuch ha σ|=GO. The e o e he lis in poin 2 canno become emp y and, since he algo i hm e mi- na es, in some s ep an objec O0such ha (O0) = will be conside ed. Then SATG(F) = hO0i 6= . Soundness P oo . I SATG(F) = hOi hen (O) = and, by P4, γ(O)|=GO. Then, by he p ope y no ed in he comple eness p oo , in e e y lis conside ed in poin 2 exis s O0such ha γ(O)|=GO0. The e o e, his holds o he ini ial lis conside ed hi(F)i, i.e., γ(O)|=G i(F), and, by P2,γ(O)|=F. 7 2.2. Seman ic Tableaux We now show how he seman ic ableaux me hod can be seen as a p oposi ional ans o ma ion sys em, and how a simple SAT-p o e based on his me hod can be seen as a pa icula ins ance o he algo i hm SATG. Le us i s o e iew he p oposi ional ableaux me hod, ollowing he desc ip ion gi en in [8]. This me hod is a e u a ion sys em: o p o e ha a o mula Fis alid, i s a s wi h a ini e ee wi h only one node labeled wi h ¬Fand applies a se o expansion ules un il i gene a es a con adic ion. F om a mo e cons uc i e poin o iew, he me hod ies o build a model o he o mula ¬F. I his is no possible, hen Fis alid. The ableaux expansion ules a e concisely p esen ed using he uni o m no a ion [19]1. Using his no a ion, non-li e al o mulas a e classi ied as doubly nega ed, α- o mulas o β- o mulas, as we show in he ollowing ables: Double nega ion componen ¬¬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 No e ha he α- o mulas a e equi alen o he conjunc ion o hei componen s α1and α2, he β- o mulas a e equi alen o he disjunc ion o hei componen s β1and β2, and he doubly nega ed o mulas a e equi alen o hei unique componen . The me hod ac s as ollows. Le Tbe a ini e ee, wi h i s nodes labeled wi h p oposi ional o mulas, and θa b anch in Twi h an oc- cu ence o a non-li e al o mula F. I Fis ¬¬X, hen he b anch θis ex ended adding a new node labeled wi h X. I Fis an α- o mula, hen he b anch θis ex ended adding wo nodes labeled wi h he componen s α1and α2o he o mula. I Fis a β- o mula, hen he b anch θis ex ended p oducing wo b anches a he end, each one wi h a node labeled, espec i ely, wi h he componen s β1and β2o he o mula. A b anch θis (a omically) closed i he e exis wo nodes in θlabeled wi h complemen a y (li e al) o mulas. The me hod is applied un il 1We ex end he uni o m no a ion o include equi alence. 8 e e y b anch is closed. In his case he o iginal o mula Fis alid. I he e is a non closed b anch θsuch ha e e y occu ence o a non-li e al o mula in θhas been expanded, hen he o mula ¬Fhas a model and he o mula Fis no alid. In his case a model o ¬Fcan be buil om he li e al o mulas in θand we say ha θp o ides a model. See Figu e 1 o an example. We now desc ibe he PTS T=hOT,;T,|=Tiassocia ed wi h he seman ic ableaux me hod. In his PTS, OTis he se o ini e sequences o o mulas ( ep esen ing ableaux b anches), σ|=Tθi and only i σmakes ue e e y o mula in he b anch θ, and ;Tis he ela ion desc ibed by he ollowing ule schema a: 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: Γ ;T i Γ does no ha e non-li e al no complemen a y o mulas The ule schema a RT3,RT4and RT5co espond wi h he ableaux expansion ules p esen ed abo e. The ule schema a RT1and RT2 check i a b anch is closed and he ule RT6checks i a b anch p o ides a model. Gi en conc e e ep esen a ion, compu a ion ule, measu e and model unc ions o his PTS, we de ine a p oposi ional ableaux me hod, which we call SATT, as a conc e e e sion o he gene ic p ocedu e SATG. By Theo em 1, his p ocedu e will be sound and comple e i p ope ies P1 o P4a e e i ied. We now de ine hese ou unc ions, p o ing he p ope ies in passing. The ep esen a ion unc ion iTis de ined such ha o e e y F∈ P(Σ), iT(F) = hFi; ha is, he only b anch in he ini ial ee conside ed by he seman ic ableaux me hod. Ob iously, σ|=F⇐⇒ σ|=Ti(F) (p ope y P2). We can conside any compu a ion ule, T, such ha , o e e y b anch θ, T(θ) is he esul o applying one o he abo e ule schema a o θ, whene e such ule may be applied. Se e al e sions o he se- man ic ableaux me hod could be ep esen ed by di e en compu a ion ules. Fo example, i he ule schema a RT1and RT2ha e less p i- o i y han he o he s, hen he expansion ules a e applied un il e e y b anch is a omically closed. To inish he expansion p ocess when he b anches a e closed, he ule schema a RT1and RT2should ha e highe p io i y han he o he s. Ano he poin could be he p e e ence o de be ween he ule schema a RT3and RT4, wi hou bi u ca ion, and he ule schema a RT5, wi h makes a bi u ca ion. Taking in o accoun 9 hese ideas, we can de ine se e al compu a ion ules and hence, se e al p oposi ional heo em p o e s based on seman ic ableaux associa ed wi h he abo e PTS. In o de o de ine he measu e unc ion, we de ine he uni o m mea- su e [1]2, deno ed as u, as ollows: u(F) = 5 ∗δ↔(F) + 2 ∗(δ∧(F) + δ∨(F) + δ→(F)) + δ¬(F), whe e δ◦(F) compu es he numbe o oc- cu ences o he connec i e ◦in F. This measu e has he ollowing p ope ies: u(α1) + u(α2)< u(α), u(β1)< u(β), u(β2)< u(β) and u(X)< u(¬¬X). We de ine he measu e unc ion, µT, as he sum o he uni o m measu e o he o mulas in a b anch. By he p ope ies o u, he expansion ules educe he measu e o a b anch; he e o e θi∈ T(θ) =⇒µT(θi)< µT(θ) (p ope y P1). The uni o m no a ion ensu es ha an α(β) o mula is logically equi alen o he conjunc ion (disjunc ion) o i s componen s and a doubly nega ed o mula ¬¬Xis also logically equi alen o X. Hence, i θ;TLwi h L6= , i can be easily p o ed ha σ|=Tθ⇐⇒ ∃θi∈L, σ |=Tθi. Acco ding o ou de ini ion o compu a ion ule, his i ially implies p ope y P3. Finally, we de ine he model unc ion γTsuch ha o e e y b anch θwi hou non-li e al no complemen a y o mulas, γT(θ)|=pi and only i pis a posi i e li e al occu ing in θ. Ob iously, i T(θ) = hen γT(θ)|=Tθ(p ope y P4). Then, by Theo em 1, he algo i hm SATT e mina es o any o - mula and is comple e and sound. The algo i hm applied o he example o Figu e 1 pe o ms he ollowing s eps ( ep esen ed 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 se o ule schema a p oposed could be imp o ed o ob ain a mo e e icien p oposi ional heo em p o e om he associa ed PTS. Fo example, he ule schema a RT1could be mixed wi h he ule schema a RT2,RT3and RT4 o a oid occu ences o complemen a y o mulas. Following his idea, we ha e de ined ano he PTS T0= hOT0,;T0,|=Tiassocia ed wi h he seman ic ableaux me hod in which he p oposi ional objec s a e lis s o o mulas wi hou complemen a y elemen s and he ule schema a a e he ollowing: RT01:hΓ1,¬¬G, Γ2i;T0hi i G∈ hΓ1,Γ2i RT02:hΓ1,¬¬G, Γ2i;T0hhΓ1, G, Γ2ii i G6∈ hΓ1,Γ2i 2We ex end he measu e p o ided in [1] o include equi alence. 16 PTS. Fo example, he ule RD4could be changed o de ec he end o he educ ion p ocess when a se o clauses Sonly has pu e li e als ( hose ha only appea posi i e o nega i e in he se o clauses) and he ule RD3could be changed o choose only non-pu e li e als. 3. Fo malizing he gene ic SAT-p o e in ACL2 Now we desc ibe a ool based on he heo e ical de elopmen p esen ed in Subsec ion 2.1. This ool builds a ce i ied p oposi ional heo em p o e om a P oposi ional T ans o ma ion Sys em and i s associa ed unc ions as i was desc ibed in Algo i hm 1, whene e he p ope ies P1,P2,P3and P4a e sa is ied. I is buil on op o he ACL2 sys em. In his sec ion, we show how he gene ic de elopmen o Subsec ion 2.1 is o malized in ACL2. 3.1. A b ie in oduc ion o ACL2 ACL2 is a p og amming language, a logic o o mal easoning abou p og ams de ined in he p og amming language, and a heo em p o e suppo ing mechanized easoning in he logic. I is de eloped by J Moo e and Ma Kau mann in he Uni e si y o Texas a Aus in, con- side ed as an “indus ial-s eng h” successo o Nq hm, also known as he Boye -Moo e heo em p o e . As a p og amming language, ACL2 is an ex ension o a subse o Common Lisp, con aining mos o he applica i e pa o ha language. The ACL2 logic is a quan i ie - ee, i s -o de logic wi h equali y, desc ibing he unc ions o he p og amming language. The syn ax o e ms is ha o Common Lisp and he logic includes axioms o p oposi ional logic and o a numbe o Lisp unc ions and da a ypes. Rules o in e ence o he logic include hose o p oposi ional calculus, equali y and ins an ia ion. One impo an ule o in e ence is he p inciple o induc ion, ha pe mi s p oo s by well- ounded induc ion on he o dinal ε0. The heo y has a cons uc i e de ini ion o he o dinals up o ε0, in e ms o lis s and na u al numbe s, gi en by he p edica e e0-o dinalp and he o de e0-o d-<. By he p inciple o de ini ion (using de un), new unc ion de ini ions a e admi ed as axioms only i he e exis s a measu e in which he a gumen s o each ecu si e call dec ease wi h espec o a well- ounded ela ion, ensu ing in his way ha no inconsis encies a e in oduced by new de ini ions. Some highe o de unc ionali y is p o ided by means o he encapsula e mechanism [13] which allows he use o in oduce new 17 unc ion symbols by axioms cons aining hem o ha e ce ain p op- e ies ( o ensu e consis ency, a wi ness local unc ion ha ing he same p ope ies has o be exhibi ed). Inside an encapsula e, he p ope ies s a ed need o be p o ed o he local wi nesses, and ou side, hey wo k as assumed axioms. This mechanism beha es like an uni e sal quan i ie o e a se o unc ions abs ac ly de ined wi h i . A de i ed ule o in e ence, called unc ional ins an ia ion, gi es some ea u es o a highe o de logic by allowing o ins an ia e he unc ion symbols o a p e iously p o ed heo em, eplacing hem wi h o he unc ion symbols o lambda exp essions, p o ided i can p o e ha he eplacemen s sa is y he cons ain s on he old symbols. The ACL2 heo em p o e mechanizes he logic. The p o e is mainly based on applying simpli ica ion and induc ion. Roughly speak- ing, when he p o e ies o p o e a conjec u e, i simpli ies he o mula. I i ob ains , hen he conjec u e is p o ed. O he wise, i guesses an (o en sui able) induc ion scheme, and ecu si ely ies o p o e he subgoals gene a ed. The heo em p o e is au oma ic in he sense ha once submi ed a conjec u e (by he command de hm), he use can no longe in e ac wi h he sys em. Bu in a wide sense, he p o e is in e ac i e: non- i ial esul s o en ail o be p o ed unless he use p e iously p o es lemmas ha can be used in subsequen p oo s as ew i ing ules. In his way, he use can help he p o e o ind a p econcei ed hand p oo . This is he way we ha e in e ac ed wi h he sys em o ob ain he esul s p esen ed in his sec ion. Fo a de ailed desc ip ion o ACL2, we e e he eade o he ACL2 book [11]. 3.2. De ini ion o he gene ic algo i hm The i s s ep o eason in ACL2 abou he algo i hm SATG, is o de ine in he ACL2 logic he unc ions in oduced by he gene ic amewo k p esen ed in Sec ion 2.1. The names o hese ACL2 unc ions and hei in ended meanings a e shown in he ollowing able: gen-objec -p(O)O∈ O gen- ep (F)i(F) gen-comp- ule(O) (O) gen-dis - al(σ, O)σ|=GO gen-model(O)γ(O) gen-measu e(O)µ(O) gen-selec (ls ) selec s an elemen om a lis ls These unc ions a e no in oduced in he ACL2 logic using he p inciple o de ini ion. Since hey a e gene ic, we de ine hem by means 18 o he encapsula e mechanism, cons aining hem o ha e ce ain p ope ies3. In his case, he p ope ies abou he gene ic unc ions a e he ollowing4: Assump ion: gen-objec -p-gen- ep p oposi ional-p(F)→gen-objec -p(gen- ep (F)) Assump ion: gen-objec -p-gen-comp- ule gen-objec -p(O1)∧(O2∈gen-comp- ule(O1)) →gen-objec -p(O2) Assump ion: e0-o dinalp-gen-measu e e0-o dinalp(gen-measu e(O)) Assump ion: P1 O2∈gen-comp- ule(O1) →gen-measu e(O2)<gen-measu e(O1) Assump ion: P2 p oposi ional-p(F) →(gen-dis - al(σ,gen- ep (F)) ↔models(σ,F)) Assump ion: P3 gen-objec -p(O)∧(gen-comp- ule(O)6= ) →(gen-dis - al(σ,O) ↔gen-dis - al-lis (σ,gen-comp- ule(O))) Assump ion: P4 gen-objec -p(O)∧(gen-comp- ule(O) = ) →gen-dis - al(gen-model(O), O) Assump ion: gen-selec -membe consp(ls )→(gen-selec (ls )∈ls ) The i s h ee p ope ies s a e ha he unc ions gen- ep , gen-comp- ule and gen-measu e ake alues as expec ed, when ac ing on elemen s o hei in ended domains. The p ope ies named P1,P2, P3 and P4 a e he co esponding o maliza ion o he p ope ies P1, P2,P3and P4, espec i ely, as de ined in he hypo hesis o Theo em 1. 3The local wi nesses a e i ele an o he de ini ion o he gene ic algo i hm and he p oo o i s p ope ies, so we omi hem he e. 4The exp essions p o ided o ACL2 a e w i en in Common Lisp no a ion bu , o imp o e hei legibili y, we p esen hem he e using a “in ix” no a ion. 19 The unc ions p oposi ional-p and models a e de ined in a p e ious ACL2 o maliza ion abou he syn ax and seman ics o p oposi ional logic; hey de ine, espec i ely, he p oposi ional o mulas and models o o mulas. The unc ion gen-dis - al-lis can be seen as a gene al- ized disjunc ion o he p edica e gen-dis - al ac ing on he objec s o a lis . The symbol <deno es he “less han” ela ion be ween o dinals. Finally, no e ha we also in oduce a unc ion gen-selec , ha selec s an elemen om any non-emp y lis . This unc ion is needed in he de ini ion o he gene ic SAT algo i hm. Once he unc ions o ou gene ic amewo k ha e been in o- duced, we de ine in ACL2 he unc ion gene ic-sa , implemen ing he algo i hm SATG: De ini ion: gene ic-sa -ls (O-ls ) = i endp(O-ls ) hen nil (1) else le * Obe gen-selec (O-ls ), (2) es be emo e-one(gen-selec (O-ls ), O-ls ), expansion be gen-comp- ule(O) (3) in i expansion = hen lis (O) (4) else gene ic-sa -ls (expansion @ es ) Measu e: gen-measu e-ls (O-ls ) Well ounded ela ion: <mul De ini ion: gene ic-sa (F) = gene ic-sa -ls (lis (gen- ep (F))) whe e he symbol @ is he “append” ope a ion be ween lis s. No e ha he main unc ion o his algo i hm is gi en by he e- cu si e unc ion gene ic-sa -ls , ac ing on a lis o objec s o be expanded. This unc ion implemen s he while loop in he de ini ion o SATG. The e mina ion o his loop is jus i ied by he measu e gen-measu e-ls (O-ls ) and he mul ise well- ounded ela ion <mul. We will explain mo e abou his issue in he nex subsec ion. When a ule o he o m hO, iis applied o a selec ed objec O, he algo i hm e u ns a single on lis con aining O(4). Acco ding o he p ope y assumed abou he unc ion gen-model, his objec has a dis inguished alua ion. Thus, e u ning he objec is use ul o p o ide a model o he inpu o mula. On he o he hand, when he e a e no mo e objec s o be expanded, he algo i hm e u ns , ep esen ed as he ACL2 symbol nil (1). This algo i hm is le unspeci ied in wo aspec s: i s , no conc e e compu a ion ule is de ined by he gene ic unc ion gen-comp- ule (3); 20 second, he objec o which he expansion ule is applied, selec ed by he abs ac ly de ined unc ion gen-selec , is no speci ied (2). 3.3. Te mina ion As i was poin ed ou in Subsec ion 3.1, new unc ion de ini ions a e admi ed in ACL2 only i he e exis s a well- ounded measu e in which he a gumen s o each ecu si e call dec ease. In he case o he unc ion gene ic-sa -ls he heu is ics o ACL2 a e no able o ind a sui able e mina ion a gumen , so we mus explici ly p o ide a measu e on i s a gumen an show ha his measu e dec eases in e e y ecu si e call wi h espec o a well- ounded ela ion. The only p ede ined well- ounded ela ion in ACL2 is e0-o d-<, implemen ing he usual o de be ween o dinals less han ε0. The unc- ion e0-o dinalp ecognizes hose ACL2 objec s ep esen ing such o dinals. I we wan o de ine a new well- ounded ela ion in ACL2, we ha e o explici ly p o ide a mono one o dinal unc ion, and p o e he co esponding o de -p ese ing heo em (see [11] o de ails). To show e mina ion o gene ic-sa -ls , we ollow he lines desc ibed in he in o mal p oo gi en in Sec ion 2.1. The measu e associa ed o i s a gumen is gi en by a unc ion gen-measu e-ls ha compu es he lis o he o dinal measu es o he objec s o a gi en lis . This measu e dec eases wi h espec o he mul ise ela ion induced by e0-o d-<. Since e0-o d-< is well- ounded, so is i s induced mul ise ela ion [7]. A o mal p oo o he well- oundedness o he mul ise ela ion induced by gi en well- ounded ela ion was o malized in he ACL2 logic in [17], whe e he de mul ool was also de eloped. This ool au oma ically gene a es he de ini ions and p o e he heo ems needed o in oduce in ACL2 he mul ise ela ion induced by a gi en well- ounded ela ion. In ou case, we only need he ollowing de mul call: (de mul (e0-o d-< nil e0-o dinalp e0-o d-<- n nil nil)) This au oma ically gene a es he de ini ion o mul-e0-o d-<, (de- no ed as <mul in he ollowing), implemen ing he mul ise ela ion on ini e mul ise s (lis s) o o dinals induced by he ela ion e0-o d-<. And i also au oma ically p o es he heo ems needed o in oduce his ela ion as a well- ounded ela ion in ACL2. See de ails abou he de mul syn ax in [17]. The main e mina ion p ope y o gene ic-sa -ls is gi en by he ollowing heo em, es ablishing ha he measu e gen-measu e-ls de- c eases in e e y ecu si e call wi h espec o he well- ounded ela ion <mul: 21 Theo em: gene ic-sa -ls - e mina ion-p ope y le * Obe gen-selec (O-ls ), es be emo e-one(gen-selec (O-ls ), O-ls ), expansion be gen-comp- ule(O) in consp(O-ls )∧(expansion 6= ) →gen-measu e-ls (expansion @ es ) <mul gen-measu e-ls (O-ls ) Ha ing p o ed his heo em (and gi en ha <mul is well- ounded, as i was au oma ically p o ed by he abo e call o de mul) he de ini ion o gene ic-sa -ls is shown o be e mina ing and i is admi ed in he logic (and he e o e, he de ini ion o gene ic-sa ). 3.4. Soundness and comple eness The ollowing heo ems es ablish he o mal p ope ies o he unc ion gene ic-sa (soundness and comple eness): Theo em: soundness-gene ic-sa p oposi ional-p(F)∧gene ic-sa (F) →models(gene ic-mod(F), F) Theo em: comple eness-gene ic-sa p oposi ional-p(F)∧models(σ,F)→gene ic-sa (F) Due o he lack o exis en ial quan i ica ion in he ACL2 logic, he soundness heo em has o be o mula ed by explici ly gi ing a model o he o mula F. This model can be easily ob ained om he esul e u ned by he gene ic-sa p ocedu e, as de ined by he unc ion gene ic-mod: De ini ion: gene ic-mod(F) = i consp(gene ic-sa (F)) hen gen-model( i s (gene ic-sa (F))) else nil The abo e wo heo ems o malize Theo em 1 in ACL2. They a e p o ed along he lines o he in o mal p oo gi en in Sec ion 2.1, basically i s p o ing by induc ion analogous p ope ies abou gene ic-sa -ls . O cou se, he p ope ies assumed abou he gene ic unc ions showed in he Subsec ion 3.2 play a c ucial ole. See de ails o he mechanical p oo in [16]. 22 4. Ins an ia ing he gene ic amewo k Conc e e SAT-p o e s will be gi en by de ining conc e e coun e pa s o he abs ac ly de ined unc ions gi en in Subsec ion 3.2. Wi h hese conc e e unc ions, one can de ine conc e e e sions o he algo i hm gene ic-sa . We can also ob ain conc e e e sions o he e mina ion, sound- ness and comple eness heo ems: i he assumed p ope ies abou he gene ic unc ions a e e i ied by he conc e e unc ions, hen by unc- ional ins an ia ion we can easily conclude e mina ion, soundness and comple eness o he conc e e SAT-p o e . 4.1. An o e iew o he ins an ia ion p ocess We desc ibe in his sec ion how we pe o m he ins an ia ion p ocess in o de o ob ain a ce i ied speci ic SAT-p o e as a conc e e ins an ia- ion o he gene ic amewo k. Fi s o all, we need a conc e e e sion o he gene ic unc ions gi en in Subsec ion 3.2. Le us assume, o ex- ample, ha we ha e a PTS such ha i s associa ed unc ions a e gi en by unc ions named objec -p, ep ,comp- ule,dis - al,model, measu e and selec , conc e e coun e pa s o he gene ic unc ions de ined in Subsec ion 3.2, and e lec ing he gi en PTS. We also need he unc ions dis - al-lis , a gene alized disjunc ion o he p edica e dis - al o e a lis o objec s, and objec -lis -p, a ecognize o p ope (null e mina ed) lis s o objec s. The ollowing s eps would ha e o be pe o med in o de o ob ain a ce i ied SAT-p o e : 1. The abo e conc e e coun e pa s o he gene ic unc ions ha e o be de ined in ACL2. We will assume ha hese unc ions a e execu able ( ha is, hey a e no de ined ia encapsula e). 2. Conc e e e sions o he assumed p ope ies abou he gene ic unc ions (gi en in Subsec ion 3.2) ha e o be p o ed. 3. The conc e e coun e pa s o he de i ed unc ions (wi h he inal goal o de ining he conc e e e sion o he unc ion gene ic-sa ), ha e o be de ined. No e ha hese unc ions will be execu able. 4. Finally, conc e e e sions o he e mina ion, soundness and com- ple eness heo ems ha e o be o mula ed and p o ed by unc ional ins an ia ion om he gene ic heo ems. The same p ocedu e would ha e o be done o e e y conc e e in- s an ia ion o he gene ic amewo k, so i makes sense o use a ool o 23 mechanize his p ocess o some ex en . In pa icula , he las wo s eps can be comple ely au oma ed. In [14], we desc ibe a use ool ha we de eloped o ins an ia e gene ic ACL2 heo ies. This ool u ns ou o be a aluable help in his con ex , whe e we ha e de eloped a gene ic heo y abou SAT-p o e s and we wan o ins an ia e he heo y o ob ain conc e e, o mally e i ied and execu able SAT-p o e s. This ool mainly consis s o a mac o named de -gene ic- heo y, which ecei es as a gumen a s ing iden i ying he heo y and a se- quence o ACL2 e en s (de ini ions and heo ems), some o which a e labeled o be ins an ia ed. When an ACL2 book5de eloping a gene ic heo y is c ea ed, we include a call o his mac o. The e ec o he mac o call is o de ine ano he mac o ha au oma ically builds conc e e e en s as ins ances o he gene ic e en s, and o ins uc he p o e o es ablish he gene a ed heo ems by unc ional ins an ia ion o he gene ic ones ( hus, hey a e au oma ically p o ed). Fo example, in he book ha o malizes he gene ic amewo k o SAT-p o e s (as desc ibed in he p e ious sec ion), we include he ollowing: (de -gene ic- heo y *gene ic-sa * <e en s>) He e <e en s> is a sequence con aining he e en s co esponding o he gene ic de ini ions and heo ems ha can be ins an ia ed by o he ACL2 books. In pa icula , he de ini ion o gene ic-sa and he heo ems es ablishing i s p ope ies. When his mac o call is execu ed, i de ines a new mac o ha ecei es as inpu a unc ional subs i u ion, gene a es he co esponding unc ional ins an ia ion o he ins an iable e en s. Fo example, once he unc ions implemen ing he conc e e coun- e pa s o he gene ic unc ions a e de ined and we ha e p o ed ha hey e i y he assumed p ope ies, we include he book wi h he gene ic SAT-p o e o maliza ion. A ha poin , a mac o de ins ance-*gene ic-sa * is au oma ically de ined, and we can use his mac o o au oma ically gene a e ins an ia ed e en s o he conc e e SAT-p o e , as ollows: (de ins ance-*gene ic-sa * ((gen-objec -p objec -p) 5A collec ion o ACL2 de ini ions and p o ed heo ems is usually s o ed in a ce i ied ile o e en s (a book in he ACL2 e minology), ha can be included in o he books. 24 (gen-objec -lis -p objec -lis -p) (gen- ep ep ) (gen-dis - al dis - al) (gen-dis - al-lis dis - al-lis ) (gen-comp- ule comp- ule) (gen-selec selec ) (gen-measu e measu e) (gen-model model)) "-conc e e") No e ha his mac o ecei es as inpu a unc ional subs i u- ion, associa ing e e y unc ion o he gene ic amewo k wi h i s conc e e coun e pa . No e ha he unc ions objec -lis -p and dis - al-lis mus also be included. I also ecei es a s ing, used o name he new e en s gene a ed, by appending i o he name o he o iginal e en . Fo example, in he abo e call, we used he p e ix "-conc e e". The esul o his mac o call is he au oma ic gene a ion o he e en s needed o de ine and e i y in ACL2 he conc e e SAT-p o e . As a con- sequence, he de ini ion o a unc ion named gene ic-sa -conc e e is gene a ed, as a unc ional ins ance o gene ic-sa . And also he ollowing heo ems, es ablishing he soundness and comple eness o gene ic-sa -conc e e, a e au oma ically gene a ed and p o ed: Theo em: soundness-gene ic-sa -conc e e p oposi ional-p(F)∧gene ic-sa -conc e e(F) →models(gene ic-mod-conc e e(F), F) Theo em: comple eness-gene ic-sa -conc e e p oposi ional-p(F)∧models(σ,F) →gene ic-sa -conc e e(F) No e ha , once he conc e e coun e pa s o he gene ic unc ions e i ying he p ope ies showed in Subsec ion 3.2 a e p o ed, no addi- ional in e ac i e p oo e o is needed o de ine and e i y he conc e e and execu able SAT-p o e . 4.2. A ableaux based SAT-p o e Along he lines o Subsec ion 2.2, we ha e de ined in ACL2 se e al ableaux based ins an ia ions o he gene ic amewo k. Fo ha pu pose we ha e de ined a ableaux e sion o he gene ic unc ions gi en in Subsec ion 3.2: ableaux-objec -p, ableaux- ep , 25 ableaux-comp- ule, ableaux-dis - al, ableaux-model, ableaux-measu e and ableaux-selec . Fo he i s ableaux based SAT-p o e , hese unc ions a e de ined as sugges ed in Subsec ion 2.2. Fo example, he de ini ion o he com- pu a ion ule is he ollowing ( ecall ha in his case, objec s a e lis s o p oposi ional o mulas, ep esen ing b anches in a ableau): De ini ion: ableaux-comp- ule(θ) = i closed- ableau(θ) hen nil RT1 else le Fbe one- o mula(θ) θ0be emo e(F,θ) in i doubly-neg-p(F) hen lis (add(neg-neg-componen (F),θ0)) RT2 elsei al a- o mula-p(F) hen lis (add(componen -1(F), add(componen -2(F),θ0)))) RT3 elsei be a- o mula-p(F) hen lis (add(componen -1(F),θ0)), add(componen -2(F),θ0))) RT4 else RT5 He e he unc ion closed- ableau checks i a b anch has comple- men a y o mulas. In his case, he emp y lis is e u ned. O he wise, a o mula is selec ed using he unc ion one- o mula, and he b anch is expanded acco ding o he ype o he o mula selec ed, as desc ibed by he ules ;T. No e ha his compu a ion ule implemen s a s a egy o applying he ableaux expansion ules in a p e e ence o de . This o de is im- plici ly gi en by he unc ion one- o mula. Any o he s a egy could ha e been de ined, p o ided ha he p ope ies assumed abou he gene ic unc ions could be p o ed o he conc e e coun e pa s. In his case, hese p ope ies a e p o ed easily, excep o P3 and P4, which a e somewha mo e elabo a e. Once he assumed p ope ies in he gene ic amewo k ha e been p o ed o he ableaux case, we can au oma ically ins an ia e he gene ic SAT-p o e algo i hm as we ha e desc ibed in he p e ious subsec ion. As a esul , we ob ain a ce i ied unc ion implemen ing he algo i hm SATTdiscussed in Sec ion 2.2. We ha e also conside ed he imp o ed PTS T0p esen ed in he las pa ag aphs o Sec ion 2.2. In his case objec s a e lis s o o mulas wi hou complemen a y elemen s and he compu a ion ule is de ined applying he ans o ma ions o ;T0in he o de p esen ed in Sec ion