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