Fo mal p oo s abou ew i ing using ACL2
José-Luis Ruiz-Reina, José-An onio Alonso, Ma ía-José Hidalgo and
F ancisco-Jesús Ma ín-Ma eos
Depa amen o de Ciencias de la Compu ación e In eligencia A i icial, Escuela Técnica Supe io
de Ingenie ía In o má ica, Uni e sidad de Se illa, A da. Reina Me cedes, s/n. 41012 Se illa, Spain
E-mails: {j uiz,jalonso,mjoseh, ma in}@cs.us.es
We p esen an applica ion o he ACL2 heo em p o e o eason abou ew i e sys ems
heo y. We desc ibe he o maliza ion and ep esen a ion aspec s o ou wo k using he i s -
o de , quan i ie - ee logic o ACL2 and we ske ch some o he main poin s o he p oo e o .
Fi s , we p esen a o maliza ion o abs ac educ ion sys ems and hen we show how his
abs ac ion can be ins an ia ed o es ablish esul s abou e m ew i ing. The main heo ems
we mechanically p o ed a e Newman’s lemma ( o abs ac educ ions) and Knu h–Bendix
c i ical pai heo em ( o e m ew i ing).
Keywo ds: heo em p o ing, ACL2, ew i ing, o mal e i ica ion
1. In oduc ion
Fo mal, mechanically checked p oo s no only p o ide e i ica ion o ma hema ical
esul s bu encou age close examina ion and deepe unde s anding o hose esul s. We
epo in his pape he s a us o ou wo k on he applica ion o he ACL2 heo em p o e
o eason abou abs ac educ ions and e m ew i ing sys ems heo y; con luence, local
con luence, Noe he iani y, no mal o ms and o he ela ed concep s ha e been o mal-
ized in he ACL2 logic and some esul s abou abs ac educ ions and e m ew i ing
ha e been mechanically p o ed, including Newman’s lemma and Knu h–Bendix c i ical
pai heo em.
ACL2 [8] is bo h a logic and a mechanical heo em p o ing sys em suppo ing i ,
de eloped by J Moo e and M. Kau mann. The ACL2 logic is an exis en ially quan i ie -
ee, i s -o de logic wi h equali y. ACL2 is also a p og amming language, an ap-
plica i e subse o Common Lisp. The sys em e ol ed om he Boye –Moo e heo em
p o e , also known as Nq hm.
The no ion o ew i ing o simpli ica ion is a c ucial componen in symbolic com-
pu a ion: simpli ica ion p ocedu es a e needed o ans o m complex objec s in o de o
ob ain equi alen bu simple objec s and o compu e unique ep esen a ions o equi a-
lence classes (see, o example, [5]). Since ACL2 is also a p og amming language, his
wo k can be seen as a i s s ep o ob ain e i ied execu able (and e icien , i possible)
This wo k has been suppo ed by DGES/MEC: P ojec TIC2000-1368-CO3-02.
Common Lisp code o componen s o symbolic compu a ion sys ems and equa ional
heo em p o e s. Al hough a ully e i ied implemen a ion o such a sys em is cu en ly
imp ac ical, se e al basic algo i hms can be mechanically “ce i ied” and in eg a ed as
pa o he whole sys em.
We also show he e how a weak logic like he ACL2 logic (no quan i ica ion, no
in ini e objec s, no highe o de a iables, e c.) can be used o ep esen , o malize, and
mechanically p o e non i ial heo ems. In his pape , we place emphasis on desc ibing
he o maliza ion and ep esen a ion aspec s o ou wo k and we also highligh some o
he main poin s o he p oo e o . 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.
We u ge he in e es ed eade o see he comple e de elopmen , a ailable on he web a
URL h p://www.cs.us.es/˜j uiz/acl2- ew . This pape is an ex ended
and e ised e sion o [15,17].
The es o he pape is o ganized as ollows. Sec ions 1.1 and 1.2 p esen a b ie
desc ip ion o ACL2 and an in o mal p esen a ion o he heo y o abs ac educ ions
and e m ew i ing, espec i ely. In sec ion 2 we p esen a o maliza ion o abs ac e-
duc ions in he ACL2 logic, including a p oo o Newman’s lemma. In sec ion 3 we
desc ibe he ins an ia ion o he abs ac o maliza ion p esen ed in he p e ious sec ion
o he case o e m ew i ing educ ions. We also p esen a p oo o Knu h–Bendix c i i-
cal pai heo em and a p oo o decidabili y o equa ional heo ies desc ibed by comple e
e m ew i ing sys ems. Finally, in sec ion 4, we d aw some conclusions and discuss u-
u e wo k.
1.1. The ACL2 sys em
We b ie ly desc ibe he e he ACL2 heo em p o e and i s logic. The bes in oduc-
ion o ACL2 is [8]. To ob ain mo e backg ound on ACL2, see he ACL2 use ’s manual
in [9]. A desc ip ion o he main p oo echniques used in Nq hm, also used in ACL2,
can be ound in [3].
1.1.1. The logic
ACL2 s ands o A Compu a ional Logic o Applica i e Common Lisp. The ACL2
logic is a quan i ie - ee, i s -o de logic wi h equali y, desc ibing an applica i e subse
o Common Lisp. The syn ax o e ms is ha o Common Lisp [19] (we will assume ha
he eade is amilia wi h his language). The 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 include hose
o p oposi ional calculus, equali y, and ins an ia ion. By he p inciple o de ini ion,new
unc ion de ini ions (using de un) a e admi ed as axioms only i he e exis s an o dinal
measu e in which he a gumen s o each ecu si e call (i any) dec ease, hus p o ing i s
e mina ion. This ensu es ha no inconsis encies a e in oduced by new de ini ions.
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-<.One
impo an ule o in e ence is he p inciple o induc ion, ha pe mi s p oo s by induc ion
on ε0.
In addi ion o he de ini ion p inciple, he encapsula ion p inciple (using encap-
sula e) allows he use o in oduce new unc ion symbols by axioms cons aining
hem o ha e ce ain p ope ies. To ensu e consis ency, wi ness unc ions ha ing he
same p ope ies ha e o be exhibi ed. Wi hin he scope o an encapsula e, p ope -
ies s a ed wi h de hm need o be p o ed o he wi nesses; ou side, hose heo ems
wo k as assumed axioms. The unc ions pa ially de ined wi h encapsula e can be
seen as second o de a iables, ep esen ing unc ions wi h hose p ope ies. A de i ed
ule o in e ence, unc ional ins an ia ion, allows some kind o second-o de easoning:
heo ems abou cons ained unc ions can be ins an ia ed wi h unc ion symbols i hey
a e known o ha e he same p ope ies (see [10]).
1.1.2. The heo em p o e
The ACL2 heo em p o e is inspi ed by Nq hm, bu has been conside ably im-
p o ed. The main p oo echniques used by he p o e a e simpli ica ion and induc ion.
Simpli ica ion is a p ocess combining e m ew i ing wi h some decision p ocedu es (lin-
ea a i hme ic, ype se easone , e c.). Sophis ica ed heu is ics o disco e ing an (o en
sui able) induc ion scheme is one o he key poin s in he success o ACL2 and i s p e-
decesso . A collec ion o 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.
The command de hm s a s a p oo a emp , and, i i succeeds, he heo em
is s o ed as a ule (in mos cases, a ew i ing ule). The heo em p o e is au oma ic
in he sense ha once de hm is in oked, he use can no longe in e ac wi h he
sys em. Howe e , in a deepe sense, he sys em is in e ac i e. Ve y o en, non i ial
p oo s a e no ound by he sys em in a i s a emp and hen he use has o guide he
p o e by adding lemmas and de ini ions, used in subsequen p oo s as ules. Inspec ion
o ailed p oo s is e y use ul o ind hose lemmas needed o “p og am” he sys em
in o de o ge he mechanical p oo o a non i ial esul . This kind o in e ac ion is
called “The Me hod” by he au ho s o he sys em (see [8]). Thus, he ole o he use
is impo an : a ypical p oo e o consis s o o malizing he p oblem in he logic and
helping he p o e o ind a p econcei ed hand p oo by means o a sui able se o ew i e
ules. The mechanical p oo s o he esul s p esen ed he e we e ca ied ou ollowing
“The Me hod”.
1.2. Abs ac educ ions and e m ew i ing sys ems
This sec ion p o ides a sho in oduc ion o basic concep s and de ini ions om
ew i ing heo y used in his pape . A comple e desc ip ion can be ound in [1].
An abs ac educ ion is simply a bina y ela ion →de ined on a se A. We will
deno e as ←,↔,∗
→and ∗
↔ espec i ely he in e se ela ion, he symme ic closu e,
he e lexi e- ansi i e closu e and he equi alence closu e. The ollowing concep s a e
de ined wi h espec o a educ ion ela ion →.Anelemen xis in no mal o m (o
i educible) i he e is no zsuch ha x→z. We say ha xand ya e joinable (deno ed
as x↓y) i he e exis s usuch ha x∗
→u∗
←y. We say ha xand ya e equi alen i
x∗
↔y.
An impo an p ope y o s udy abou educ ion ela ions is he exis ence o unique
no mal o ms o equi alen objec s. A educ ion ela ion has he Chu ch–Rosse p op-
e y i e e y wo equi alen objec s a e joinable. An equi alen p ope y is con luence:
o all x,u, such ha u∗
←x∗
→ , henu↓ . In e e y educ ion ela ion wi h he
Chu ch–Rosse p ope y he e a e no dis inc and equi alen no mal o ms. I in addi-
ion he ela ion is no malizing (i.e., e e y elemen has a no mal o m, deno ed as x↓)
hen x∗
↔yi x↓= y↓. P o ided no mal o ms a e compu able and iden i y in Ais
decidable, hen he equi alence ela ion ∗
↔is decidable, by means o a es o equali y
o no mal o ms.
Ano he impo an p ope y is e mina ion: a educ ion ela ion is e mina ing (o
Noe he ian) i he e is no in ini e educ ion sequence x0→x1→x2→ ···.Ob i-
ously, e e y Noe he ian educ ion is no malizing. The Chu ch–Rosse p ope y can be
localized when he educ ion is e mina ing. In ha case an equi alen p ope y is local
con luence: o allx,u, such ha u←x→ , henu↓ . This esul is known as
Newman’s lemma.
An impo an ype o educ ion ela ion is de ined on he se T(,X)o i s o de
e ms o a gi en language, whe e is a se o unc ion symbols, and Xis a se o
a iables. In his con ex , an equa ion isapai o e msl= . The educ ion ela ion
de ined by a se o equa ions Eis de ined as: s→E i he e exis l= ∈Eand a
subs i u ion σo he a iables in l( he ma ching subs i u ion) such ha σ(l)is a sub e m
o sand is ob ained om sby eplacing he sub e m σ(l) o σ( ). This educ ion
ela ion is o g ea in e es in uni e sal algeb a because i can be p o ed ha E|= s=
i s∗
↔E . This implies decidabili y o e e y equa ional heo y de ined by a se o
axioms Esuch ha →Eis e mina ing and locally con luen . To emphasize he use o
he equa ion l= om le o igh as desc ibed abo e, we w i e l→ and alk abou
ew i e ules.A e m ew i ing sys em (TRS) is a se o ew i e ules. Unless deno ed
o he wise, Eis always a se o equa ions (equa ional axioms) and Ris a e m ew i ing
sys em.
Local con luence is decidable o ini e and no malizing TRSs: joinabili y has only
o be checked o a ini e numbe o pai o e ms, called c i ical pai s, accoun ing o he
mos gene al o ms o local di e gence (see [1] o a p ecise de ini ion). The c i ical pai
heo em s a es ha a TRS is locally con luen i all i s c i ical pai s a e joinable. Thus,
he Chu ch–Rosse p ope y o e mina ing TRSs is a decidable p ope y: i is enough
o check i e e y c i ical pai has a common no mal o m. In ha case, he TRS is said
o be comple e and can be used o decide i s equa ional heo y. I a e mina ing TRS
has a c i ical pai wi h di e en no mal o ms, he e is s ill a chance o ob ain a decision
p ocedu e o i s equa ional heo y, adjoining ha equa ion as a new e mina ing ew i e
ule. This is he basis o he well-known comple ion algo i hm (see [1] o de ails).
In he sequel, we desc ibe he o maliza ion o hese p ope ies in he ACL2 logic
and some poin s o hei mechanical p oo . Fo he es o he pape , when we alk abou
“p o e” we mean “mechanically p o e using ACL2”.
2. Fo malizing abs ac educ ions in ACL2
One possible way o ep esen abs ac educ ion ela ions in he ACL2 logic could
be simply o de ine hem as bina y Boolean unc ions, using encapsula e o s a e
hei p ope ies. Ne e heless, we adop ed a sligh ly di e en app oach, in o de o s ess
he “ educ ion” poin o iew: i x→y, mo e impo an han he ela ion be ween xand
yis he ac ha yis ob ained om xby applying some kind o ans o ma ion o ope -
a o . In i s mos abs ac o mula ion, we can iew a educ ion as a bina y unc ion ha ,
gi en an elemen and an ope a o , e u ns ano he objec , pe o ming a one-s ep educ-
ion. Think o example o equa ional educ ions: elemen s in ha case a e i s -o de
e ms and ope a o s a e he objec s cons i u ed by a posi ion (indica ing he sub e m
eplaced), an equa ion ( he ule applied) and a subs i u ion ( he ma ching subs i u ion).
O cou se no any ope a o can be applied o any elemen . Thus, a second com-
ponen in his o maliza ion is needed: a Boolean bina y unc ion o es i i is legal o
apply an ope a o o an elemen . Finally, a hi d componen is in oduced: since com-
pu a ion o no mal o ms equi es sea ching o legal ope a o s o apply, we will need
a una y unc ion ha when applied o an elemen e u ns a legal ope a o , whene e i
exis s, o nil o he wise (a educibili y es ).1
The abo e conside a ions lead us o o malize he concep o abs ac educ ions
in ACL2, using h ee pa ially de ined unc ions: educe-one-s ep,legal and
educible. This can be done wi h he ollowing encapsula e (do s a e used o
omi local e en s2and echnical de ails, as in he es o he pape ):
(encapsula e
(( educe-one-s ep (x op) )
(legal (x op) )
( educible (x) ))
...
(de hm legal- educible-1
(implies ( educible x) (legal x ( educible x))))
(de hm legal- educible-2
(implies (no ( educible x)) (no (legal x op))))
...)
1I is possible o p o e some o he heo ems p esen ed he e wi hou any e e ence o a educibili y es ( o
example, Newman’s lemma). See he web page.
2The speci ic wi ness unc ions de ini ions a e i ele an o ou discussion, since ou side he encapsu-
la e only he nonlocal p ope ies a e used.

The i s pa o e e yencapsula e is a signa u e desc ip ion o he nonlocal
unc ions pa ially de ined. No e ha ( educe-one-s ep x op) is he elemen
ob ained applying he ope a o op o x. The unc ion legal is he applicabili y es ,
i.e., (legal x op) is no nil i i is legal o apply op o x.And educible is
he educibili y es : ( educible x) is a legal ope a o applicable o xwhene e
such ope a o exis s, nil o he wise (we a e assuming ha nil does no ep esen any
ope a o ).
The wo heo ems assumed abo e as axioms a e minimal equi emen s o e e y
educ ion we de ined: i u he p ope ies ( o example, local con luence, con luence o
Noe he iani y) we e assumed, hey ha e o be s a ed inside he encapsula e.Thisis
a e y abs ac amewo k o o malize educ ions in ACL2. We hink ha hese h ee
unc ions cap u e he basic abs ac ea u es e e y educ ion has. On he one hand, a
p ocedu al aspec : he compu a ion o no mal o ms, applying ope a o s un il i educible
objec s a e ob ained. On he o he hand, a decla a i e aspec : e e y educ ion ela ion
desc ibes i s equi alence closu e. Rep esen ing educ ions in his way, we can de ine
concep s like he Chu ch–Rosse p ope y, local con luence o Noe he iani y and e en
p o e non i ial heo ems like Newman’s lemma, as we will see.
To ins an ia e his gene al amewo k, conc e e ins ances o educe-one-s ep,
legal and educible ha e o be de ined and he p ope ies assumed he e as axioms
mus be p o ed o hose conc e e de ini ions. By unc ional ins an ia ion, esul s abou
abs ac educ ions can hen be easily expo ed o conc e e cases (as we will see o he
equa ional case).
2.1. Equi alence and p oo s
Due o he cons uc i e na u e o he ACL2 logic, in o de o de ine x∗
↔y,we
ha e o include an a gumen wi h a sequence o s eps x=x0↔x1↔x2···↔xn=y.
This is done by he unc ion equi -p de ined in igu e 1. (equi -p x y p) is
i pis an abs ac p oo 3jus i ying ha x∗
↔y. Thismeans ha pis a sequence o
legal s eps connec ing xand y, whe e each p oo s ep is a s uc u e4 -s ep wi h
ou ields: el 1,el 2 ( he elemen s ela ed by he s ep), di ec (a boolean alue
indica ing i he s ep is di ec o in e se) and ope a o . A p oo s ep is legal (as
de ined by p oo -s ep-p) i one o i s elemen s is ob ained by applying i s ope a o
(which mus be legal) o he o he elemen , in he di ec ion indica ed by di ec .Two
abs ac p oo s jus i ying he same equi alence will be said o be equi alen .
The Chu ch–Rosse p ope y and local con luence can be ede ined wi h espec o
he o m o abs ac p oo s (sec ions 2.2 and 2.3). Fo ha pu pose, we de ine (omi ed
he e) unc ions o ecognize p oo s wi h pa icula shapes ( alleys and local peaks):
local-peak-p ecognizes p oo s o he o m ←x→uand s eps- alley
ecognizes p oo s o he o m ∗
→x∗
←u.
3O simply a p oo i ha e minology does no a ise con usion wi h p oo s done using he ACL2 sys em.
4We used he de s uc u e ool de eloped by B. B ock [4].
(de s uc u e -s ep di ec ope a o el 1 el 2)
(de un p oo -s ep-p (s)
(le ((el 1 (el 1 s)) (el 2 (el 2 s))
(op (ope a o s)) (di ec (di ec s)))
(and ( -s ep-p s)
(implies di ec
(and (legal el 1 op)
(equal ( educe-one-s ep el 1 op)
el 2)))
(implies (no di ec )
(and (legal el 2 op)
(equal ( educe-one-s ep el 2 op)
el 1))))))
(de un equi -p (x y p)
(i (endp p)
(equal x y)
(and (p oo -s ep-p (ca p))
(equal x (el 1 (ca p)))
(equi -p (el 2 (ca p)) y (cd p)))))
Figu e 1. De ini ion o p oo s and equi alence.
2.2. The Chu ch–Rosse p ope y and decidabili y
We desc ibe how we o malized and p o ed he decidabili y o an equi alence e-
la ion desc ibed by a Chu ch–Rosse and no malizing educ ion. Valley p oo s can be
used o e o mula e he de ini ion o he Chu ch–Rosse p ope y: a educ ion is Chu ch–
Rosse i o e e y abs ac p oo he e exis s an equi alen alley p oo . Since he
ACL2 logic is quan i ie - ee, he exis en ial quan i ie in his s a emen has o be e-
placed by a Skolem unc ion, which we call ans o m- o- alley. The concep
o being no malizing can also be e o mula ed in e ms o abs ac p oo s: a educ ion
is no malizing i o e e y elemen he e exis s an abs ac p oo o an equi alen i e-
ducible elemen . This p oo is gi en by he (Skolem) unc ion p oo -i educible
(no e ha we a e no assuming Noe he iani y ye ). P ope ies de ining a Chu ch–Rosse
and no malizing educ ion a e encapsula ed as shown in igu e 2, i em (a).
The unc ion -equi es s i no mal o ms a e equal. The no mal o m o an
elemen xis de ined o be he las elemen o (p oo -i educible x):
(de un no mal- o m (x)
(las -o -p oo x (p oo -i educible x)))
(de un -equi (x y)
(equal (no mal- o m x) (no mal- o m y)))
;;; (a) De ini ion o Chu ch-Rosse no malizing educ ion:
(encapsula e
((legal (x op) ) ( educe-one-s ep (x op) )
( educible (x) ) ( ans o m- o- alley (x) )
(p oo -i educible (x) ))
.....
(de hm Chu ch-Rosse -p ope y
(le (( alley ( ans o m- o- alley p)))
(implies (equi -p x y p)
(and (s eps- alley alley)
(equi -p x y alley)))))
.....
(de hm no malizing
(le * ((p-x-y (p oo -i educible x))
(y (las -o -p oo x p-x-y)))
(and (equi -p x y p-x-y)
(no ( educible y))))))
;;; (b) Main heo ems p o ed:
(de hm i -C-R-- wo-i educible-connec ed-a e-equal
(implies (and (equi -p x y p)
(no ( educible x))
(no ( educible y)))
(equal x y)))
(de hm -equi -sound
(implies ( -equi x y)
(equi -p x y (make-p oo -common-n- x y))))
(de hm -equi -comple e
(implies (equi -p x y p) ( -equi x y))
Figu e 2. Chu ch–Rosse and no malizing implies decidabili y.
To p o e decidabili y o a Chu ch–Rosse and no malizing ela ion, i is enough
o p o e ha -equi is a comple e and sound algo i hm deciding he equi a-
lence ela ion desc ibed by he educ ion ela ion. See igu e 2, i em (b).Wealso
include he main lemma used, s a ing ha he e a e no dis inc equi alen i e-
ducible elemen s. No e also ha soundness is exp essed in e ms o a Skolem unc-
ion make-p oo -common-no mal- o m (de ini ion omi ed), which cons uc s a
p oo jus i ying he equi alence. These heo ems a e p o ed qui e easily, wi hou much
guidance om he use . The main poin he e is ha he induc ion scheme sugges ed
by he unc ion equi -p (and mechanically gene a ed by he sys em), u ns ou o be
e y use ul in p o ing p ope ies abou he ela ion ∗
↔: i esembles he in ui i e idea o
“induc ion on he numbe o s eps”.
2.3. Noe he iani y, local con luence and Newman’s lemma
A ela ion is well ounded on a se Ai e e y nonemp y subse has a minimal
elemen . A es ic ed no ion o well- oundedness is buil in o ACL2, based on he ol-
lowing me a- heo em: a ela ion on a se Ais well- ounded i he e exis s a unc ion
F:A→O d such ha x<y⇒F(x) < F(y),whe eO d is he class o all o di-
nals. In ACL2, once a ela ion is p o ed o sa is y hese equi emen s (and he heo em
is s o ed as a well- ounded- ela ion ule), i can be used in he admissibili y
es o ecu si e unc ions. A gene al well- ounded pa ial o de el can be de ined
in ACL2 as shown in igu e 3, i em (a). Since only o dinals up o ε0a e o malized
in he ACL2 logic, a limi a ion is imposed in he maximal o de ype o well- ounded
ela ions ha can be ep esen ed. Consequen ly, ou o maliza ion su e s om he same
es ic ion.5
In igu e 3, i em (b) a gene al de ini ion o a Noe he ian and locally con luen e-
duc ion ela ion is p esen ed.6Local con luence is easily exp essed in e ms o he shape
o abs ac p oo s in ol ed: a ela ion is locally con luen i o e e y local peak p oo
he e is an equi alen alley p oo . This alley p oo is assumed o be gi en by a unc ion
named ans o m-local-peak. As o Noe he iani y, ou o maliza ion elies on
he ollowing me a- heo em: a educ ion is Noe he ian i and only i i is con ained in a
well- ounded pa ial o de ing. Thus, he gene al well- ounded ela ion el p e iously
p esen ed is used o jus i y Noe he iani y o he gene al educ ion ela ion de ined: o
e e y elemen xsuch ha a legal ope a o op can be applied o, hen applying op o
xusing educe-one-s ep, p oduces an elemen less han x(wi h espec o el).
The s anda d p oo o Newman’s lemma ound in he li e a u e [1], shows con-
luence by Noe he ian induc ion based on he Noe he ian educ ion ela ion. Ne e -
heless, he o mal p oo we ob ained is di e en , in luenced by ou abs ac p oo
app oach. I is inspi ed by he one gi en by Klop in [11]. In ou o maliza ion, we
show ha he educ ion ela ion has he Chu ch–Rosse p ope y7by de ining a unc ion
ans o m- o- alley and p o ing ha o e e y p oo p,( ans o m- o-
- alley p) is an equi alen alley p oo . This unc ion is de ined o i e a i ely ap-
ply eplace-local-peak (which eplaces a local peak subp oo by he equi alen
p oo gi en by ans o m-local-peak), un il he e a e no local peaks. This can
be seen as a no maliza ion p ocess ac ing on abs ac p oo s. See de ini ion in igu e 3,
i em (c).
5Ne e heless, no pa icula p ope ies o ε0a e used in ou p oo s, excep well- oundedness.
6Name con lic s wi h he unc ions p esen ed in he p e ious and nex sec ions a e a oided using Common
Lisp packages.
7No e ha we do no need o deal wi h con luence since he Chu ch–Rosse p ope y, an equi alen concep ,
is p o ed wi h he same e o .
;;; (a) TRS wi h joinable c i ical pai s:
(encapsula e
((RLC () ) ( ans o m-cp (l1 1 pos l2 2) ))
...
(de hm RLC- ew i e-sys em ( ew i e-sys em (RLC)))
(de hm RLC-joinable-c i ical-pai s
(implies
(and (membe (cons l1 1) (RLC))
(membe (cons l2 2) (RLC))
(posi ion-p pos l1)
(no ( a iable-p (occu ence l1 pos))))
(le * ((cp- (cp- l1 1 pos l2 2))
( alley-cp ( ans o m-cp l1 1 pos l2 2)))
(implies
cp-
(and (eq-equi -p
(lhs cp- ) ( hs cp- ) alley-cp (RLC))
(s eps- alley alley-cp)))))))
;;; (b) Theo em p o ed:
(de un ans o m-eq-local-peak (p) ...)
(de hm c i ical-pai - heo em
(le (( alley ( ans o m-eq-local-peak p)))
(implies (and (eq-equi -p 1 2 p (RLC))
(local-peak-p p))
(and (s eps- alley alley)
(eq-equi -p 1 2 alley (RLC))))))
Figu e 5. The c i ical pai heo em.
3.5. Reduc ion o de ings
In o de o o malize e mina ion p ope ies o e m ew i ing sys ems we ely on
he well-known concep o educ ion o de ing, i.e., well- ounded o de ing being s able
(closed unde ins an ia ion) and compa ible (closed unde eplacemen o sub e ms). We
used he ollowing cha ac e iza ion: a e m ew i ing sys em R e mina es i he e exis s
a educ ion o de  ha sa is ies l o all l→ ∈R. In igu e 6, encapsula ion is

(encapsula e
(( ed< ( 1 2) ) ( n- ed< ( e m) ))
....
(de hm ed<-well- ounded- ela ion
(and (e0-o dinalp ( n- ed< 1))
(implies ( ed< 1 2)
(e0-o d-< ( n- ed< 1) ( n- ed< 2))))
: ule-classes :well- ounded- ela ion)
(de hm ed<-s able
(implies ( ed< 1 2)
( ed< (ins ance 1 sigma)
(ins ance 2 sigma))))
(de hm ed<-compa ible
(implies (and (posi ion-p pos e m) ( ed< 1 2))
( ed< ( eplace- e m e m pos 1)
( eplace- e m e m pos 2))))
(de hm ed<- ansi i e
(implies (and ( ed< x y) ( ed< y z)) ( ed< x z))))
(de un noe he ian- ed< (TRS)
(i (endp TRS)
(le (( ule (ca TRS)))
(and ( ed< ( hs ule) (lhs ule))
(noe he ian- ed< (cd TRS)))))
Figu e 6. A educ ion o de ed<.
used o (pa ially) de ine a unc ion ed<, assumed o be a educ ion o de . The unc ion
(noe he ian- ed< TRS) is de ined o es i ed< jus i ies e mina ion o TRS.
Once ed< has been assumed o be a educ ion o de ing and he unc ion noe-
he ian- ed< has been de ined, we p o ed ha he educ ion ela ion →Ris e mi-
na ing, whene e Ris a TRS such ha (noe he ian- ed< R) ( his esul is needed
o expo Newman’s lemma o he equa ional case):
(de hm R-Noe he ian-i -subse p-o - ed<
(implies (and (noe he ian- ed< R)
(eq-legal e m op R))
( ed< (eq- educe-one-s ep e m op) e m)))
Al hough he (pa ial) de ini ion o he educ ion o de ing ed< gi en in igu e 6
wo ks well om a heo e ical poin o iew, he main d awback in his o maliza ion
o educ ion o de ings is ha i can be di icul o p o e ha a pa icula o de ing ( o
example, a pa h o de ing o a Knu h–Bendix o de ing [1]) is a educ ion o de ing, since
an o dinal measu e n- ed< has o be gi en explici ly.
3.6. Comple e e m ew i ing sys ems and decidabili y
As a consequence o he esul s p esen ed so a , and using unc ional ins an ia ion,
we can o malize and p o e decidabili y o he equa ional heo y desc ibed by a comple e
TRS. In he ollowing we desc ibe he assump ions needed o de ine a comple e TRS.
Again using encapsula e we (pa ially) de ine a e m ew i ing sys em (RC)
assumed o be comple e: (RC) is e mina ing (jus i ied by ed<) and e e y c i ical
pai ob ained om ules in (RC) ha e a common no mal o m (see igu e 7). In his
o maliza ion, he concep s o c i ical pai s and no mal o ms a e implemen ed by he
unc ions cp- (desc ibed in sec ion 3.4) and RC-no mal- o m, espec i ely.
The unc ion RC-no mal- o m is de ined o compu e no mal o ms wi h espec
o he e m ew i ing sys em (RC). I i e a i ely applies he unc ion - educe un il
a no mal o m is ound. The exp ession ( - educe e m TRS), whose de ini ion
we omi he e, pe o ms one s ep o ew i ing, whene e i is possible. I a e ses e m
o ind a sub e m subsumed by he le -hand side o a ule in TRS. When such a sub-
e m is ound, i is eplaced by he co esponding ins ance o he igh -hand side o he
ule. I i is no ound, hen - educe e u ns nil (and he e o e e m is in no mal
o m). Those p ope ies o - educe we e mechanically e i ied. No e ha a e i ied
subsump ion algo i hm is needed o ha pu pose.
I is wo h poin ing ha a unc ion compu ing he no mal o m o a e m wi h
espec o a TRS would no be admi ed in he ACL2 logic, since e mina ion is no
assu ed in gene al. Ins ead, we assume (RC) o be e mina ing and we de ine no mal
o m calcula ion wi h espec o (RC).10
Ha ing assumed he p ope ies o igu es 6 and 7, we can de ine a unc ion
RC-equi alen ( es ing equali y o no mal o ms) and hen p o e ha i p o ides
a comple e and sound algo i hm o decide he equa ional heo y o (RC):
(de un RC-equi alen ( 1 2)
(equal (RC-no mal- o m 1) (RC-no mal- o m 2)))
(de hm RC-equi alen -comple e
(implies (eq-equi -p 1 2 p (RC))
(RC-equi alen 1 2)))
10 Al hough his de ini ion is sui able om a o mal poin o iew, he main d awback is ha
ha RC-no mal- o m is no execu able. Ne e heless, we can de ine an execu able unc ion
(no mal- o m-n n e m R) ha applies (a mos ) n educ ion s eps o e m wi h espec o
he TRS R. In p ac ice, his can be used o compu e no mal o ms.
(encapsula e
((RC () ))
...
(de hm RC- ew i e-sys em ( ew i e-sys em (RC)))
(de hm RC-Noe he ian- ed< (noe he ian- ed< (RC)))
(de un RC-no mal- o m ( e m)
(decla e (xa gs :measu e e m
:well- ounded- ela ion ed<))
(le (( ed ( - educe e m (RC))))
(i ed (RC-no mal- o m (unpack ed)) e m)))
(de hm RC-common-n- -c i ical-pai s
(implies
(and (membe (cons l1 1) (RC))
(membe (cons l2 2) (RC))
(posi ion-p pos l1)
(no ( a iable-p (occu ence l1 pos))))
(le ((cp- (cp- l1 1 pos l2 2)))
(implies
cp-
(equal (RC-no mal- o m (lhs cp- ))
(RC-no mal- o m ( hs cp- ))))))))
Figu e 7. A comple e e m ew i ing sys em (RC).
(de hm RC-equi alen -sound
(implies (RC-equi alen 1 2)
(eq-equi -p
1 2
(RC-make-p oo -common-n- 1 2) (RC))))
The p oo o he wo heo ems abo e is s aigh o wa d (al hough some elabo a ed)
by means o unc ional ins an ia ion o he p e ious heo ems p esen ed. The ollowing
is pa o he unc ional subs i u ion used in his ins an ia ion, associa ing o he unc ions
desc ibing an abs ac educ ion he co esponding unc ions o he equa ional educ ion
associa ed o (RC):
...
( educe-one-s ep eq- educe-one-s ep)
( educible (lambda ( e m)
(eq- educible e m (RC))))
(legal (lambda ( e m op)
(eq-legal e m op (RC))))
(equi -p (lambda ( 1 2 p)
(eq-equi -p 1 2 p (RC))))
...
An impo an poin in his decidabili y heo em is ha he e i ied decision algo-
i hm RC-equi alen does no deal wi h equa ional p oo s, equa ional p oo s eps o
equa ional ope a o s. This is an example o composi ional easoning, o how o eason
abou an implemen a ion by using ules ha ans o m some unc ions in o he unc ions
(o en less e icien ) ha a e easie o eason abou .
No e ha in his case he unc ions eq- educible and eq- educe-one-s ep
p o ides a way o pe o m one s ep o ew i ing, whene e i is possible: gi en a e m
and a TRS, apply eq- educible o ob ain an equa ional ope a o and, i non-nil,
apply his ope a o o he e m using eq- educe-one-s ep.I heTRSis e mi-
na ing, hen his me hod can be applied i e a i ely un il a no mal o m is ob ained. This
de ini ion o no mal o m is app op ia e o easoning. Fo example, i u ns ou o be
use ul when we de ine an equa ional coun e pa o p oo -i educible, a unc-
ion ob aining an equa ional p oo connec ing e e y elemen o i s no mal o m, ha is
needed o expo by unc ional ins an ia ion he decidabili y esul o sec ion 2.2. Ob-
iously, his no mal o m calcula ion can be op imized in se e al ways. Fo example, a
unc ion compu ing no mal o ms nei he needs o build an equa ional ope a o in e e y
ew i ing s ep no a e se he e ms wice, sea ching o a legal equa ional ope a o , and
hen applying he educ ion s ep. As we desc ibed abo e, - educe is a mo e e icien
(al hough no op imal) e sion o one-s ep ew i ing. The main poin he e is ha we
used he mo e heo e ical e sion o eason abou no mal o m calcula ion, which u ned
ou o be simple . La e on, we p o ed heo ems ela ing he beha io o - educe
wi h eq- educible and eq- educe-one-s ep, showing he equi alence wi h
he imp o ed e sion o no mal o m calcula ion, and hen we s a ed he inal e sion o
he heo em using - educe.
4. Conclusions and u he wo k
We ha e p esen ed an applica ion o he ACL2 sys em o o malize and eason
abou ew i e sys ems heo y. This is a case s udy o using he ACL2 sys em as a me a-
language o o malize p ope ies o objec p oo sys ems (abs ac educ ions and equa-
ional logic in his case) in i . Ou o maliza ion has he ollowing main ea u es:
•Abs ac educ ion ela ions and hei p ope ies a e s a ed in a e y gene al ame-
wo k, as explained in sec ion 2. Func ional ins an ia ion is ex ensi ely used o expo
esul s om he abs ac case o he equa ional case.
•The concep s o abs ac p oo s and equa ional p oo s a e key no ions in ou wo k, as
i has been poin ed epea edly. P oo s a e ea ed as objec s ha can be ans o med
o ob ain new p oo s and his poin o iew has g ea in luence bo h in o maliza ion
and easoning.
•Composi ional easoning is used, e i ying some unc ions by using ew i e ules ha
ans o m hem in o he unc ions, o en less e icien , ha a e easie o eason abou .
We hink ha he esul s p esen ed he e a e impo an o wo easons. F om a he-
o e ical poin o iew, i is shown how a weak logic can be used o o malize p ope ies
o TRSs. F om a p ac ical poin o iew, his is an example o how o mal me hods can
help in he design o symbolic compu a ion sys ems. Usually, ew i ing echniques a e
applied o he design o p oo p ocedu es in au oma ed deduc ion. We show how bene i s
can be ob ained in he e e se di ec ion: au oma ed deduc ion used as a ool o “ce i y”
componen s o symbolic compu a ion sys ems.
Since ACL2 is also a p og amming language, compu ing and p o ing asks can
be mixed. As a esul o his o maliza ion, we ob ained a numbe o basic unc ions
in e m ew i ing, execu able and e i ied in ACL2; o example, ma ching, uni ica ion,
compu a ion o c i ical pai s o applica ion o educ ion s eps wi h espec o a e m
ew i ing sys em. We e i ied he gua ds o all hese unc ions, ensu ing in his way ha
hey a e execu able in any complian Common Lisp (wi h he app op ia e iles loaded).
I should be s essed ha p o ing non i ial esul s in a heo em p o e like ACL2
is no i ial. A use expe in bo h he heo em p o e and he subjec domain is needed
(maybe ha is he eason why many o he published o mal p oo s a e abou o mal sys-
ems). As claimed in [8], di icul ies come om “ he complexi y o he whole en e p ise
o o mal p oo s”, a he han om he complexi y o ACL2. A ypical p oo e o con-
sis s o o malizing he p oblem and guiding he p o e o a p econcei ed “hand p oo ”,
by decomposing he p oo in o in e media e lemmas. Ne e heless, p oo s can be sim-
ple i a good lib a y o p e ious esul s (books in he ACL2 e minology) is used. We
hink ou wo k p o ides a good collec ion o books o be eused in u he e i ica ion
e o s.
The p oo desc ibed he e has been s uc u ed in h ee collec ion o books (see he
web page), ch onologically de eloped in he ollowing o de (e e y book needs esul s
om i s p edecesso ):
1. Books abou abs ac educ ions: abs ac -p oo s con ains basic de ini ions
and p ope ies abou abs ac p oo s, con luence p o es he decidabili y o
he equi alence ela ion desc ibed by a Chu ch–Rosse and no malizing educ ion,
newman is he p oo o Newman’s lemma and local-con luence isap oo ,
by unc ional ins an ia ion, o decidabili y o he equi alence ela ion desc ibed by a
e mina ing and locally con luen educ ion ela ion.

2. Books abou equa ional heo ies and ew i ing: equa ional- heo ies con ains
he de ini ion and main p ope ies o he equa ional heo y gi en by a se o equa ional
axioms and ew i ing de elops he no ions o educibili y, educ ion o de ings
and one-s ep ew i ing.
3. The p oo o he c i ical pai heo em is in he book c i ical-pai s and decid-
abili y o he equa ional heo y o a comple e TRS is p o ed in kb-decidabili y.
Table 1 gi es some quan i a i e in o ma ion on he p oo . The i s column con ains
he name o he book. The nex h ee columns show he numbe o lines (including
commen s), he numbe o de ini ions and he numbe o heo ems in each book. These
numbe s can gi e an idea o he g anula i y o ou p oo . We should say ha hese
sizes can be educed, bu some imes we p e e ed o spli de ini ions and heo ems o
he sake o cla i y. We also included a i h column wi h he numbe o heo ems ha
needed hin s om he use : he es o he heo ems we e p o ed au oma ically by he
sys em. Toge he wi h he numbe o heo ems, his can gi e an idea o he deg ee o
au oma ion o he p oo s. Mos o he hin s gi en a e o disabling o enabling ules and
o using ins ances o p e ious heo ems.
I is clea om he able ha he main p oo e o was done o p o e Newman’s
lemma and he c i ical pai heo em. I should be emphasized also ha , al hough no
lis ed in he able, he books abou i s -o de e ms [14] and mul ise ela ions [16] a e
c ucial in ou de elopmen .
Some ela ed wo k has been done in he o maliza ion o abs ac educ ion e-
la ions in o he heo em p o ing sys ems, mos ly as pa o o maliza ions on he
λ-calculus. Fo example, Hue [7] in he Coq sys em o Nipkow [13] in Isabelle/HOL.
A compa ison is di icul because ou goal was di e en and, mo e impo an , he logics
in ol ed a e signi ican ly di e en : ACL2 logic is a much weake logic han hose o
Coq o HOL. A mo e ela ed wo k is Shanka [18], using Nq hm. Al hough his wo k is
on he conc e e educ ion ela ion o λ-calculus and he does no deal wi h he abs ac
case, some o his ideas a e e lec ed in ou wo k.
Table 1
Quan i a i e in o ma ion on he p oo s.
Book Lines De ini ions Theo ems Hin s
abs ac -p oo s 284 16 17 0
con luence 387 12 31 7
newman 993 15 53 10
local-con luence 464 19 14 6
equa ional- heo ies 543 11 29 8
ew i ing 720 13 38 9
c i ical-pai s 2129 43 112 26
kb-decidabili y 500 16 18 7
To al 6020 145 312 73
To ou knowledge, no o maliza ion o e m ew i ing sys ems has been done ye
and, consequen ly, he o mal p oo s o hei p ope ies p esen ed he e a e he i s ones
we know pe o med using a heo em p o e .
In addi ion o ex end he lib a y o esul s abou e m ew i ing sys ems, he e a e
also se e al ways in which he wo k p esen ed he e can be u he de eloped, mos ly de-
o ed o imp o e e iciency o he e i ied algo i hms and o apply he esul s o conc e e
equa ional heo ies:
•In o de o ob ain ce i ied decision p ocedu es o some conc e e equa ional heo ies,
wo k has o be done o o malize in ACL2 well-known e mina ing e m o de ings ( e-
cu si e pa h o de ings, Knu h–Bendix o de ings, e c.). As commen ed in sec ion 3.5,
maybe some p oblems will a ise due o he es ic ed no ion o Noe he iani y sup-
po ed by ACL2.
•The wo k p esen ed in [12] sugges s ano he applica ion o his wo k: o he heo em
p o e s can be combined wi h ACL2 in o de o ob ain mechanically e i ied decision
algo i hms o some equa ional heo ies.
•Al hough a ully e i ied equa ional easoning sys em is cu en ly imp ac ical, i
would be desi able o imp o e he e iciency o he algo i hms ( o example, using
be e da a s uc u es). Composi ional easoning can be used o eason abou hese
imp o ed algo i hms.
•Ou o iginal mo i a ion when we began his o maliza ion (and now ou goal in he
long e m) is o ob ain a ce i ied comple ion p ocedu e w i en in Common Lisp. We
hink he wo k p esen ed he e is a good s a ing poin .
Re e ences
[1] F. Baade and T. Nipkow, Te m Rew i ing and All Tha (Camb idge Uni e si y P ess, Camb idge,
1998).
[2] L. Bachmai , Canonical Equa ional P oo s (Bi khäuse , New Yo k, 1991).
[3] R. Boye and JS. Moo e, A Compu a ional Logic Handbook, 2nd ed. (Academic P ess, New Yo k,
1998).
[4] B. B ock, de s uc u e o ACL2 e sion 2.0, Technical Repo , Compu a ional Logic, Inc.
(1997).
[5] B. Buchbe ge and R. Loos, Algeb aic simpli ica ion, in: Compu e Algeb a, Symbolic and Algeb aic
Compu a ion. Compu ing Supplemen um 4 (1982).
[6] G. Hue , Con luen educ ions: abs ac p ope ies and applica ions o e m ew i ing sys ems, Jou nal
o he ACM 27(4) (1980) 797–821.
[7] G. Hue , Residual heo y in λ-calculus: a o mal de elopmen , Jou nal o Func ional P og amming 4
(1994) 475–522.
[8] M. Kau mann, P. Manolios and JS. Moo e, Compu e -Aided Reasoning: An App oach (Kluwe Aca-
demic, Do d ech , 2000).
[9] M. Kau mann and JS. Moo e, ACL2 Ve sion 2.5 (2000) a ailable a h p://www.cs.
u exas.edu/use s/moo e/acl2/acl2-doc.h ml.
[10] M. Kau mann and JS. Moo e, S uc u ed heo y de elopmen o a mechanized logic, Jou nal o
Au oma ed Reasoning 26(2) (2001) 161–203.
[11] J.W. Klop, Te m ew i ing sys ems, in: Handbook o Logic in Compu e Science (Cla endon P ess,
Ox o d, 1992).
[12] W. McCune and O. Shumsky, I y: a p ep ocesso and p oo checke o i s -o de logic, in:
Compu e -Aided Reasoning: ACL2 Case S udies (Kluwe Academic, Do d ech , 2000) chap e 16.
[13] T. Nipkow, Mo e Chu ch–Rosse p oo s, Jou nal o Au oma ed Reasoning 26(1) (2001) 51–66.
[14] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, Mechanical e i ica ion o a ule based
uni ica ion algo i hm in he Boye –Moo e heo em p o e , in: AGP’99 Join Con e ence on Decla a-
i e P og amming (1999) pp. 289–304.
[15] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, A mechanical p oo o Knu h–Bendix
c i ical pai heo em (using ACL2), in: FTP’2000 (Thi d Wo kshop on Fi s -O de Theo em P o ing),
Technical Repo 5-2000, Fachbe ich e In o ma ik, Uni e si ä Koblenz-Landau (2000).
[16] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, Mul ise ela ions: a ool o p o ing e -
mina ion, in: Second ACL2 Wo kshop, Technical Repo TR-00-29, Compu e Science Depa amen ,
Uni e si y o Texas (2000).
[17] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, Fo malizing ew i ing in he ACL2 heo-
em p o e , in: AISC’2000 (Fi h In e na ional Con e ence A i icial In elligence and Symbolic Com-
pu a ion), Lec u e No es in Compu e Science, Vol. 1930 (Sp inge , Be lin, 2001) pp. 92–103.
[18] N. Shanka , A mechanical p oo o he Chu ch–Rosse heo em, Jou nal o he ACM 35(3) (1988)
475–522.
[19] G.L. S eele, Common Lisp he Language, 2nd ed. (Digi al P ess, 1990).