P og ess Repo : Te m Dags Using S objs ?
J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo and F.-J. Ma ´ın-Ma eos
h p://www.cs.us.es/{~j uiz,~jalonso,~mjoseh,~ ma in}
Depa amen o de Ciencias de la Compu aci´on e In eligencia A i icial.
Escuela T´ecnica Supe io de Ingenie ´ıa In o m´a ica, Uni e sidad de Se illa
A da. Reina Me cedes, s/n. 41012 Se illa, Spain
Abs ac . We explo e in his pape he use o e icien da a s uc u es o implemen ope -
a ions on i s -o de e ms, ha can be o mally e i ied. Speci ically, we p esen he s a us
o ou wo k on de ining and e i ying a uni ica ion algo i hm ac ing on e ms ep esen ed
as di ec ed acyclic g aphs (dags). This implemen a ion is done using single h eaded objec s
(s objs) o s o e a dag ep esen ing he uni ica ion p oblem.
In oduc ion
In [6], we desc ibed a o mal app oach, using ACL2, o he me a- heo y o equa ional easoning
and e m ew i ing sys ems. As a by-p oduc o his wo k, we ob ained e i ied implemen a ions
o some basic ope a ions on i s -o de e ms, including ma ching, an i–uni ica ion, uni ica ion,
no mal o ms wi h espec o e m ew i ing sys ems and c i ical pai compu a ion.
In ha o maliza ion, e ms a e ep esen ed as lis s, using p e ix no a ion. Such ep esen a ion
is specially well sui ed o he au oma ion o easoning abou e ms (in pa icula , in p oo s by
induc ion on he s uc u e o e ms) bu om he execu ion e iciency poin o iew i is no he
bes solu ion: due o he applica i e na u e o he ACL2 language, some ope a ions ( o example,
he applica ion o a subs i u ion o a e m) needs o ebuild e ms in o de o compu e hei esul s.
The s anda d app oach o deal wi h his p oblem is o s o e e ms as di ec ed acyclic g aphs
(dags), using poin e s uc u es allowing some amoun o s uc u e sha ing. Thus, ope a ions ne e
build new e ms bu me ely upda es poin e s [1]. In ACL2, des uc i e upda es can be implemen ed
using single h eaded objec s (s objs). These a e s uc u es wi h he usual applica i e seman ics
o ACL2 bu o which upda es a e implemen ed des uc i ely. To ensu e ha hese des uc i e
upda es a e consis en wi h i s applica i e seman ics, ACL2 en o ces some syn ac ic es ic ions
on he use o a s obj, which ensu es ha only one e e ence o he objec needs e e exis . See [2]
o a de ailed desc ip ion o s objs in ACL2 o [7, 8] o wo case s udies whe e s objs a e used o
de ine and e i y e icien p og ams.
Ou in en ion is o explo e he use o s objs o ep esen e m dags in ACL2, in o de o de ine
and e i y e icien ope a ions on i s -o de e ms. As a i s a emp , we epo he s a us o ou
wo k ying o implemen and e i y a uni ica ion algo i hm on e m dags. In his p og ess epo ,
we desc ibe an implemen a ion based on s objs. Al hough we ha e no ye e i ied his uni ica ion
algo i hm, we hink i is in e es ing o p esen he cu en s a us o ou wo k.
1 Uni ica ion on e m dags
In he ollowing, we will assume ha he eade is amilia wi h uni ica ion heo y [1]. The uni-
ica ion algo i hm we ha e implemen ed is based on he well-known se o ans o ma ion ules
gi en by Ma elli and Mon ana i and shown in igu e 1. This se o ules ac on pai s o sys ems
o equa ions o he o m S;U. The sys em Scan be seen as a se o pai s o e ms o be uni ied
?This wo k has been suppo ed by MCYT: P ojec TIC2000–1368–C03–02
and he sys em Uas a (pa ially) compu ed uni ie . The symbol ⊥ ep esen s uni ica ion ailu e.
S a ing wi h a pai o sys ems S;∅, hese ules can be (non-de e minis ically) applied un il ei he
a pai o sys ems ∅;Uo ⊥is ob ained. I can be p o ed ha hese ules a e e mina ing and ha
Sis uni iable i and only i ⊥is no ob ained; in ha case, Uis a mos gene al uni ie (mgu) o
S. Thus, an algo i hm o uni y wo e ms 1and 2can be designed by choosing a s a egy o
exhaus i ely apply he ules s a ing wi h he pai o sys ems { 1≈ 2};∅.
Dele e:{ ≈ } ∪ R;U⇒uR;U
Check:{x≈ } ∪ R;U⇒u⊥
i x∈ V( ) and x6=
Elimina e:{x≈ } ∪ R;U⇒uθ(R); {x≈ } ∪ θ(U)
i x∈X,x /∈ V( ) and θ={x7→ }
Decompose:{ (s1,...,sn)≈ ( 1, . . . , n)} ∪ R;U⇒u{s1≈ 1,...,sn≈ n} ∪ R;U
Clash :{ (s1,...,sn)≈g( 1,..., m)} ∪ R;U⇒s⊥, i n6=mo 6=g
O ien :{ ≈x} ∪ R;U⇒u{x≈ } ∪ R;U
i x∈X, /∈X
Fig. 1. T ans o ma ion ules
As pa o an ACL2 lib a y wi h o mal p oo s o he la ice heo e ic p ope ies o i s -o de
e ms, we de ined and e i ied a uni ica ion algo i hm based on he abo e ideas. This wo k was
ansla ed o ACL2 om a p e ious o maliza ion done in Nq hm, desc ibed in [5]. In his lib a y,
we ep esen i s -o de e ms in p e ix no a ion using lis s. Fo example, he e m (x, g(y), h(x))
is ep esen ed as ’( x (g y) (h x)). E e y consp objec can be seen as a e m wi h i s ca as
i s op unc ion symbol and i s cd as he lis o i s a gumen s. Va iables a e ep esen ed by a om
objec s. Subs i u ions a e ep esen ed as associa ion lis s and equa ions as do ed pai s o e ms.
A nai e implemen a ion o he abo e uni ica ion algo i hm can be ine icien in some si ua ions.
Conside , o example, he ollowing s anda d uni ica ion p oblem:
p(x1, . . . , xn)≈p( (x0, x0), (x1, x1), . . . , (xn−1, xn−1))
A mgu o his example is {x17→ (x0, x0), x27→ ( (x0, x0), (x0, x0)), . . .}, mapping each xi
o a comple e bina y ee o heigh i. This uni ie can be ob ained by epea edly applying he
Elimina e ule o igu e 1. Using lis s o ep esen e ms, a econs uc ion o he e ms is needed
e e y ime he ule is applied, making he algo i hm ine icien .
The s anda d app oach o deal wi h his sou ce o ine iciency is o ep esen e ms as di ec ed
acyclic g aphs (dags). Fo example, in igu e 2 we ep esen he uni ica ion p oblem gi en by he
equa ion (h(z), g(h(x), h(u))) ≈ (x, g(h(u), )). Nodes a e labeled wi h unc ion and a iable
symbols, and ou going edges connec e e y node wi h dags ep esen ing i s immedia e sub e ms.
We can na u ally iden i y he oo node o a dag e m wi h he whole e m. No e also ha he e
is also a ce ain amoun o s uc u e sha ing, a leas o he epea ed a iables.
To implemen a uni ica ion algo i hm wi h his e m ep esen a ion, he main idea is ne e
build new e ms bu only c ea e poin e s. In pa icula , he Elimina e ule can be implemen ed
adding a poin e linking he a iable wi h he e m o which his a iable is bound; in ha way no
econs uc ion o he e m is equi ed in he applica ion o a subs i u ion. In igu e 2, hese poin e s
a e ep esen ed by dashed a ows. The binding o a a iable can be de e mined by ollowing he
poin e s a e sing he g aph dep h i s , om le o igh . In his case, he subs i u ion ep esen ed
is {x7→ h(z), u 7→ h(z), 7→ h(h(z))}, which is a mgu o (h(z), g(h(x), h(u))) and (x, g(h(u), )).
z
hg g
hh h
u
x
Fig. 2. Dag ep esen a ion o (h(z), g(h(x), h(u))) ≈ (x, g(h(u), ))
2 An ACL2 implemen a ion
We desc ibe now how we use a s obj o s o e i s -o de e ms as di ec ed acyclic g aphs (we will
assume ha he eade is amilia wi h s objs [2]). We de ine he ollowing s obj con aining one
a ay ield:
(de s obj e ms-dag
(dag : ype (a ay (1000)) : esizable ))
Each node in he g aph is ep esen ed by a cell in he dag a ay o he s obj. Thus, a node in
he g aph can be iden i ied wi h an a ay index. Each cell s o es he label and he neighbo s o
each node, in he ollowing way:
–I node i ep esen s an unbound a iable x, hen (dagi i e ms-dag) con ains a do ed pai
o he o m (x. ).
–I node i ep esen s a bound a iable, hen (dagi i e ms-dag) con ains an index npoin ing
o he e m o which he a iable is bound.
–I node iis he oo node o a non- a iable e m ( 1, . . . , n), hen (dagi i e ms-dag) is a
do ed pai o he o m ( .l), whe e lis he lis o he indices co esponding o 1, . . . , n.
In his way, we can s o e a uni ica ion p oblem using he e ms-dag s obj. Fo example, i we
s o e he e m equ( (h(z), g(h(x), h(u))), (x, g(h(u), ))) (i.e., he uni ica ion p oblem o igu e 2)
he signi ican cells o he dag a ay a e1:
((EQU 1 9) (F 2 4) (H 3) (Z . T) (G 5 7) (H 6) (X . T) (H 8) (U . T)
(F 10 11) 6 (G 12 14) (H 13) 8 (V . T))
We can na u ally iden i y an a ay index wi h he whole e m whose oo node is poin ed o
by ha index. We exploi his in ui i e idea in he de ini ion o a unc ion ha applies one s ep o
he ans o ma ion ⇒ugi en in igu e 3.
Le us now desc ibe ha unc ion, called dag- ans o m-mm. In addi ion o he s obj, his
unc ion ecei es as inpu a (non-emp y) sys em So equa ions o be uni ied and a subs i u ion
U(pa ially) compu ed. Depending on he o m o he i s equa ion o S, one o he ules o
⇒uis applied. Bu he main poin he e is ha Sand Ucon ain poin e s o he e ms s o ed in
dag. In pa icula , Sis a lis o pai s o indices, and Uis a lis o do ed pai s o he o m (x
.n)whe e xis a iable symbol and nis an index poin ing o he node o which he a iable
1To p in his a ay, we a e using a unc ion ha collec s he a ay cells in a lis .
(de un dag- ans o m-mm (S U e ms-dag)
(decla e (xa gs :s objs ( e ms-dag)
:mode :p og am))
(le * ((ecu (ca S)) (R (cd S))
( 1 (dag-de e (ca ecu) e ms-dag))
( 2 (dag-de e (cd ecu) e ms-dag))
(p1 (dagi 1 e ms-dag)) (p2 (dagi 2 e ms-dag)))
(cond
((= 1 2) (m R U e ms-dag)) ;;; DELETE
((dag- a iable-p p1)
(i (occu -check 1 2 e ms-dag) ;;; CHECK
(m nil nil nil e ms-dag)
(le (( e ms-dag (upda e-dagi 1 2 e ms-dag))) ;;; ELIMINATE
(m R (cons (cons (dag-symbol p1) 2) U) e ms-dag))))
((dag- a iable-p p2)
(m (cons (cons 2 1) R) U e ms-dag)) ;;; ORIENT
((no (eq (dag-symbol p1) (dag-symbol p2))) ;;; CLASH
(m nil nil nil e ms-dag))
( (m -le (pai -a gs bool)
(pai -a gs (dag-a gs p1) (dag-a gs p2))
(i bool ;;; DECOMPOSE
(m (append pai -a gs R) U e ms-dag)
(m nil nil nil e ms-dag))))))) ;;; CLASH
Fig. 3. De ini ion o p oo s and equi alence
is bound (i.e. a subs i u ion). The unc ion e u ns a mul i alue wi h he ollowing componen s,
ob ained as a esul o he applica ion o one s ep o ⇒u: he esul ing sys em o equa ions o
be sol ed, he esul ing subs i u ion, a boolean alue (i ⊥is ob ained, his alue is nil) and he
s obj e ms-dag. See he de ini ions o he auxilia y unc ions in he ile dag-uni ica ion.lisp
o he suppo ing ma e ials. Only when Elimina e is applied, his s obj is upda ed, causing he
co esponding a iable o poin o he co esponding e m.
Once we ha e de ined he unc ion ha applies one s ep o he ans o ma ion ules, we can
de ine a unc ion ha compu es he mos gene al uni ie o wo e ms, whene e i exis s. In sho ,
his unc ion s o es bo h e ms as di ec ed acyclic g aphs in he s obj (p e iously esizing he dag
a ay), and i e a i ely applies he unc ion dag- ans o m-mm un il ei he a ailu e is de ec ed
o he e a e no mo e equa ions o be sol ed. In his case, he e u ned subs i u ion is ob ained
om he dag, ollowing he poin e s o he ins an ia ed a iables. You can see he de ini ion in
he suppo ing ma e ials ( unc ion dag-mgu in he ile dag-uni ica ion.lisp). I is in e es ing
o poin ou ha he syn ac ic es ic ions needed o de ine an ACL2 unc ion ha uses s objs
a e na u ally ensu ed in his case. In he ile dag-uni ica ion-examples.lisp we include some
execu ion examples.
I should be poin ed ou ha his algo i hm s ill has exponen ial ime complexi y, bu wi h
some echnical modi ica ions i is easy o implemen a quad a ic algo i hm. We p e e ed o use
his simple implemen a ion o desc ibe he main poin s o his wo k. Mo eo e , his uni ica ion
algo i hm is p obably he mos popula , since he wo s exponen ial case is e y uncommon in
p ac ice.
3 Commen s on he o mal e i ica ion
Al hough a he ime o his w i ing he abo e uni ica ion algo i hm has no been e i ied, we hink
i is in e es ing o poin ou some issues encoun e ed du ing he wo k comple ed up o his poin .
3.1 Di ec ed acyclic g aphs
The i s p oblem we ace when dealing wi h o mal e i ica ion o his algo i hm is o ge ACL2 o
admi he unc ion de ini ions. The unc ions desc ibed in he p e ious sec ion a e all in :p og am
mode, because some o he auxilia y unc ions used by he algo i hm a e no o al: i he g aph
s o ed in e ms-dag con ains cycles, a unc ion a e sing his g aph may no e mina e. Fo
example, he auxilia y unc ion occu -check checks i a a iable node is in he e m poin ed o
by an index, a e sing he g aph and sea ching o a a iable occu ence. This unc ion is no
e mina ing in gene al2.
One possible solu ion would be o a e se he g aph aking in o accoun he nodes al eady
isi ed, hus a oiding cyclic pa hs. Bu checking cycles du ing compu a ion would a ec he e i-
ciency o he p ocess3. Since one o ou main conce ns is e iciency, we adop a di e en app oach:
we will eason abou ou unc ions as i hey we e pa ial, only de ined on a speci ied domain. In
ou case, his domain will be he se o di ec ed acyclic g aphs.
We ha e de ined a unc ion dag-p, checking i a lis g ep esen ing a g aph (using he con en ions
explained abo e when we desc ibed he dag ield o e ms-dag) is cycle- ee. We omi i s de ini ion
he e (see he suppo ing ma e ials, book dags.lisp), bu he ollowing a e he main p ope ies we
p o ed abou i , e i ying ha (dag-p g) is nil i and only i he e is a cyclic pa h in g:
(de hm dag-p-soundeness
(implies (no (dag-p g)) (cycle-p (one-cyclic-pa h g) g)))
(de hm dag-p-comple eness
(implies (cycle-p p g) (no (dag-p g))))
The de ini ion o dag-p and he p oo o he abo e heo ems a e inspi ed by [4]. The main
di e ence wi h ha wo k is ha ou ep esen a ion o g aphs is di e en and, mo e impo an ,
ha we a e ensu ing ha he e a e no cyclic pa h wha e e he s a ing node.
I a g aph g e i ies dag-p i is possible o de ine a well- ounded measu e jus i ying ha a e s-
ing ha g aph, dep h- i s and om le o igh , s a ing om a node (o a lis o nodes) is a
e mina ing p ocess. This measu e, called measu e- ec-dag, essen ially coun s he nodes ha can
be eached om he s a ing nodes.
Ha ing de ined his measu e, we can ge ACL2 o admi unc ions wi h ecu si e de ini ions on
he s uc u e o e ms dag. Fo example, we can de ine he ollowing unc ion in he ACL2 logic:
(de pun occu -check-l ( lg x h g)
(decla e (xa gs :domain (dag-p g)
:measu e (measu e- ec-dag lg h g)))
(i lg
(le ((p (n h h g)))
(cond ((dag-bound-p p) (occu -check-l lg x p g))
((dag- a iable-p p) (= x h))
( (occu -check-l nil x (dag-a gs p) g))))
(i (endp h)
2No e also ha e en i occu -check is ne e called, he uni ica ion algo i hm can loop. Fo example, he
Decompose ule could be applied and in ini e numbe o imes.
3Ne e heless, his check could be done in a less ine icien way (see subsec ion 3.3).

nil
(o (occu -check-l x (ca h) g)
(occu -check-l nil x (cd h) g)))))
This unc ion has exac ly he same body as occu -check, he unc ion in :p og am mode used
in he uni ica ion algo i hm desc ibed abo e. Ne e heless, his unc ion is de ined in :logic mode,
so we can eason abou i . No e ha we used he de pun mac o (see [3]) o in oducing “pa ial
unc ions”. In his case, his mac o in oduces a heo em equa ing he e m (occu -check-l lg x
h g) wi h i s body, unde he hypo hesis (dag-p g), and his heo em is s o ed as a :de ini ion
ule. No e also ha he a gumen gis no a s obj; since we only need his unc ion om a logical
poin o iew, his is i ele an and simpli ies he easoning.
This kind o de ini ion is a ypical ecu si e de ini ion on he s uc u e o e ms. The unc ion
is de ined a he same ime o e ms and o lis o e ms, by mu ual ecu sion. The a gumen lg
is a lag indica ing i hhas o be conside ed as one single e m (i.e., one single poin e ) o as a
lis o e ms (i.e., a lis o poin e s). We ha e de ined (in he logic) all he auxilia y unc ions ha
does ecu sion on he s uc u e o e ms in his way, using de pun wi h domain (dag-p g).
3.2 Fo mal e i ica ion and composi ional easoning
Once we can desc ibe he uni ica ion algo i hm in he ACL2 logic, ou nex s ep will be o p o e
ha he uni ica ion algo i hm compu es a uni ie o wo e ms i and only i hey a e uni iable, and
in ha case he compu ed uni ie is a mos gene al uni ie . We s a e hese p ope ies using he lis
ep esen a ion o e ms, since he o mal heo y abou i s -o de e ms we de eloped uses e ms
ep esen ed as lis s. Bu we wan o p o e hese p ope ies abou an algo i hm wo king wi h he
dag ep esen a ion o e ms.
As we said ea lie , we had o mally e i ied a uni ica ion algo i hm based on ⇒u, using he lis
ep esen a ion o e ms. The main (and s anda d) idea is o use composi ional easoning (as in
[7]) o ansla e he p o ed p ope ies o his algo i hm o he algo i hm based on e m dags. This
means ha we ha e he ollowing p oo obliga ions:
–I he condi ions needed o apply one o he ules o ans o ma ion a e me by a uni ica ion
p oblem ep esen ed as dags, hen he same condi ions a e me by he co esponding uni ica ion
p oblem ep esen ed as lis s.
–In such case, he uni ica ion p oblem ob ained applying he ule o ans o ma ion o he dag
ep esen a ion is he same as he uni ica ion p oblem ob ained applying he same ule o he
lis ep esen a ion.
–The abo e p ope ies has o be p o ed assuming he dag-p p ope y, among o he needed
condi ions. The e o e, we will need o p o e ha hese p ope ies a e p ese ed in e e y s ep
o ans o ma ion (in pa icula , when he ans o ma ion upda es he s obj).
I is wo h poin ing ou ha he kind o s uc u al ecu sion desc ibed abo e o occu -check-l
is simila o he ecu sion we used in he de ini ion o an analogous unc ion ac ing on e ms
ep esen ed as lis s. In gene al, he e is a close ela ionship be ween de ini ions on he s uc u e o
a e m ep esen ed as a lis and he analogous de ini ion o e m dags. The e o e, we hope ha
he echnique o composi ional easoning will be e ec i e he e.
3.3 Execu ion
Al hough wi h he assis ance o he de pun mac o we can eason abou pa ial unc ions only
de ined on well- o med e m dags, he unc ions we e i y a e no e icien unc ions ope a ing on
s objs, because o he expensi e dag-p check. Fo he momen execu ion o pa ial unc ions is no
suppo ed by de pun. We hink he e a e wo al e na i es o ace wi h his si ua ion, in o de o
be con iden abou he unc ion inally used o execu ion:
•A simple app oach would be o de ine o al e sions o he unc ions de ined wi h de pun,
in oducing a coun e ha is dec emen ed in e e y ecu si e call, and ailing i his coun e
eaches 0. Thus, in his case he expensi e dag-p check is eplaced by a simple in ege es and
his o al e sions can be used o execu ion, whene e a sui ably la ge coun e is p o ided.
P e iously we would ha e o p o e ha he de pun e sion and he coun e e sion coincide
when hei a gumen s a e well- o med e m dags and he coun e is no exhaus ed.
In some cases, a sui able alue o he coun e could be compu ed, and we could p o e ha
wi h ha alue o he coun e he unc ion ne e ails when ac ing on e m dags. Fo example,
a sui able alue o e e y unc ion ha a e ses dags (like he one implemen ing he occu
check) could be he leng h o he a ay used o s o e he dag.
•A di e en app oach, simila o [8], would be o “ ake ma e s in o ou hands” and use o
execu ion unc ions in :p og am mode wi h he same body as he unc ions de ined wi h
de pun. Unlike [8], ou dag-p check is no i ele an , so we ha e o be ca e ul be o e gi ing
his “dange ous” s ep.
In o de o explo e his possibili y, we can use he gua ded domain op ion :gdomain o de pun
(see [3]). Essen ially, his means ha he domain is included as he :gua d o he wi ness
unc ion used o jus i y he in oduc ion o he pa ial unc ion de ined by de pun. In ou case,
he gua ded domain is gi en by well- o med e m dags. I hese gua ds can be e i ied, he
ecu sion is closed in he gua ded domain. We hink ha his could be a good eason o be
con iden abou his al e na i e.
4 Conclusions
We ha e p esen ed he s a us o ou wo k in he de elopmen o a e i ied uni ica ion algo i hm
ep esen ing e ms as di ec ed acyclic g aphs. Ou idea is o explo e he use o single h eaded
objec s o implemen e icien da a s uc u es o ep esen ing i s -o de e ms, allowing as exe-
cu ion and o mal e i ica ion. We ha e seen ha i is possible o implemen he algo i hm (e en
wi h he syn ac ic es ic ions en o ced by he sys em on he use o s objs). We ha e also desc ibed
how we can in oduce in o he ACL2 logic he de ini ions o unc ions de ined on he s uc u e o
a e m dag. We a e cu en ly in he p ocess o o mal e i ica ion. I his a emp is success ul,
we may conside ex ending his s udy o o he da a s uc u es and indexing echniques commonly
used in au oma ed easoning.
Re e ences
1. Baade , F. and Snyde , W. Uni ica ion heo y. Handbook o Au oma ed Reasoning, El esie Science
Publishe s, 2001.
2. Boye R.S. and Moo e J S. Single- h eaded objec s in ACL2. In URL: www.cs.u exas.edu/-
use s/moo e/publica ions/acl2-pape s.h ml#Founda ions.
3. Manolios, P. and Moo e J S. Pa ial unc ion is ACL2. In Second ACL2 Wo kshop, Technical
Repo TR-00-29, Compu e Science Depa men , Uni e si y o Texas, 2000.
4. Moo e, J S. An exe cise in g aph heo y. In Compu e -Aided Reasoning: ACL2 Case S udies,
chap e 5. Kluwe Academic Publishe s, 2000.
5. Ruiz-Reina, J., Alonso, J., Hidalgo, M., and Ma ´
ın, F. 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, pp. 289–304, 1999.
6. Ruiz-Reina, J., Alonso, J., Hidalgo, M., and Ma ´
ın, F. 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
Compu a ion), LNCS 1930, pp. 92–103. Sp inge -Ve lag, 2001.
7. Sumne s, R. Co ec ness P oo o a BDD Manage in he Con ex o Sa is iabili y Checking. In
Second ACL2 Wo kshop, Technical Repo TR-00-29, Compu e Science Depa men , Uni e si y o
Texas, 2000.
8. Wilding, M. Using a Single-Th eaded Objec o Speed a Ve i ied G aph Pa h inde . In Second ACL2
Wo kshop, Technical Repo TR-00-29, Compu e Science Depa men , Uni e si y o Texas, 2000.