A Ce ied Polynomial-Based Decision P o cedu e
o P op osi ional Logic
Inmaculada Medina-Bulo
1
,F ancisco Palomo-Lozano
1
,
and José A. Alonso-Jiménez
2
1
Depa men o Compu e Languages and Sys ems. Uni e si y o Cádiz
Esc. Sup e io de Ingenie ía de Cádiz. C/ Chile, s/n. 11003 Cádiz. Spain
{ ancisco.palomo,inmaculada.medina} @uca .es
2
Depa men o Comp. Sciences and A icial In elligence, Uni e si y o Se illa
Fac. de In o má ica y Es adís ica. A da. Reina Me cedes, s/n. 41012 Se illa, Spain
[email p o ec ed]
Abs ac .
In his pap e we p esen he o maliza ion o a decision p o-
cedu e o P op osi ional Logic based on p olynomial no maliza ion. This
o maliza ion is sui able o i s au oma ic e ica ion in an applica i e
logic like
Acl2
. This applica ion o p olynomials has b een de elop ed by
eusing a p e ious wo k on polynomial ings [19 ], showing ha a p op e
o maliza ion leads o a high le el o eusabili y. Two checke s a e de-
ned: he  s o con adic ion o mulas and he second o au ology
o mulas. The main heo ems s a e ha b o h checke s a e sound and
comple e. Mo eo e , unc ions o gene a ing mo dels and coun e exam-
ples o o mulas a e p o ided. This acili y plays also an imp o an ole
in he main p o o s. Finally, i is shown ha his allows o a highly
au oma ed p o o de elopmen .
1In o duc ion
In his pap e we p esen he main esul s ob ained h ough he de elopmen o an
au oma ed p oo o he co ec ness o a polynomial-based decision p ocedu e o
P op osi ional Logic in
Acl2
[14,15,16].
Acl2
1
is he successo o
Nq hm
[3,5],
he Boye -Mo o e heo em p o e . A concise desc ip ion o
Acl2
can be ound
in [14]. In o de o unde s and
Acl2
, i is necessa y o conside i unde h ee
die en p e sp ec i es:
1. F om a logic iewp oin ,
Acl2
is a un yp ed quan ie - ee  s -o de logic o
o al ecu si e unc ions wi h equali y.Howe e , i s
encapsula ion
p inciple
allows o some kind o highe -o de easoning.
2. F om a p og amming language iewp oin ,
Acl2
is an applica i e p og am-
ming language in which he esul o he applica ion o a unc ion is uniquely
de e mined by i s a gumen s. E e y
Acl2
unc ion admi ed unde he de -
ini ional p inciple is a
Lisp
unc ion, so you can ob ain bo h e ied and
execu able so wa e.
1
A Compu a ional Logic o Applica i e Common Lisp.
3. F om a easoning sys em iewpoin ,
Acl2
is an au oma ed easoning sys em
and i b eha es as a heu is ic heo em p o e .
Rep esen a ion issues play a ma jo ole in his wo k. We ha e ep esen ed
P op osi ional Logic o mulas in e ms o jus one Bo olean unc ion symb ol: he
h ee-place condi ional cons uc p esen in mos p og amming languages. This
is discussed in Sec . 2.1. Deni ions ela ed wi h Bo olean p olynomials a e p e-
sen ed in Sec . 2.2.
Su p isingly, p olynomial-based heo em p o ing has a long his o y.Acco ding
o H. Zhang [28], Bo ole himsel [2] was he  s o use Boolean polynomials o
ep esen logical o mulas and He b and desc ib ed a p olynomial-based decision
p o cedu e in his hesis. La e , in 1936, M. S one [23] s a ed he s ong ela ion
exis ing be ween Bo olean algeb as and Bo olean ings. Analogous esul s had
b een disco e ed, indep enden ly, in 1927 by I. I. Zhegalkin [29].
This ela ion is a he basis o he mo de n algeb aic me hods o logical
deduc ion. The algeb aic app oach b egan wi h he de elopmen by J. Hsiang
o a canonical e m- ew i ing sys em o Bo olean algeb as wi h applica ions o
 s -o de heo em p o ing [11,12]. Concu en ly,D.Kapu and P. Na end an
used G öbne bases and Buchb e ge 's algo i hm o he same pu p ose [17].
2
This
las me ho d has b een ex ended o many- alued p oposi ional logics [7,26] and i
has b een ecen ly applied o knowledge based sys ems e ica ion [18].
Se e al decision p o cedu es o p oposi ional logic ha p o duce a e iable
p o o log ha e b een implemen ed. Fo example, [9,10] ep o he de elopmen o
BDDs and S ªma ck's algo i hm as HOL de i ed ules. On he o he hand, ac ual
o mal e ica ions o decision p o cedu es a e less common. The classical wo k
om [3] con ains a e ied decision p o cedu e in
Nq hm
using IF-exp essions. A
simila p o cedu e has b een ex ac ed om a
Coq
p o o in [22]. Ano he decision
p o cedu e ob ained ia p o o ex ac ion in
Nup l
is desc ib ed in [6]. Howe e ,
none o hem is based on p olynomial no maliza ion.
Weha e no conside ed he p ossibili yo in eg a ing he decision p o cedu e
in o he heo em p o e ia eec ion, hough his is easible in
Acl2
hanks
o i s me a heo e ical ex ensibili y capabili ies [4]. A eec ed decision p o ce-
du e has b een de elop ed in [1] wi h
Nup l
. See also [8] o a c i ical su ey o
eec ion in heo em p o ing om a heo e ical and p ac ical iewp oin .
Sec ion 2.3 p esen s a ansla ion algo i hm om o mulas in o p olynomials.
Once ha sui able e alua ion unc ions ha e b een dened, his ansla ion is
shown o b e in e p e a ion-p ese ing. In Sec . 3, we e iew Hsiang's canonical
e m- ew i ing sys em (TRS) o Bo olean algeb as. A no maliza ion algo i hm
ha is no based in e m- ew i ing is also p esen ed. In Sec . 4, we p o e he
co ec ness o he decision p o cedu e o P op osi ional Logic. As he in ol ed
algo i hms a e w i en in an applica i e subse o
Common Lisp
, hey a e in-
insically execu able. Some examples o execu ion a e shown in Sec . 5.
Finally,we will discuss he deg ee o au oma ion achie ed and we will also
analyze some possible ex ensions o his wo k.
2
See also [13 ,28 ,27 ].
2 IF-Fo mulas and Bo olean Polynomials
In [20]an
Acl2
o maliza ion o IF-Fo mulas and Bo olean polynomials is p o-
p osed. Nex , he no ion o S one p olynomial o an IF- o mula is easily dened.
We e iew he e he main esul s ob ained wi h some imp o emen s.
As he condi ional cons uc
IF
is unc ionally comple e, we can ega d ou
P op osi ional Logic o mulas as IF- o mulas wi hou loss o gene ali y.In ac ,
he
Nq hm
Boye -Moo e logic and i s descendan
Acl2
dene he usual p opo-
si ional connec i es a e axioma izing
IF
. IF- o mulas a e also ela ed wi h he
OBDD algo i hm as can be seen in [21]. A BDD manage has b een ecen ly
o malized in
Acl2
[24].
2.1 IF-Fo mulas
The unde lying ep esen a ion o IF- o mulas is based on he no ion o IF-cons.
IF-conses a e weake han IF- o mulas in he sense ha hey may no ep e-
sen well- o med o mulas. We use eco d s uc u es o ep esen IF-conses. This
p o ides us wi h a weak ecognize p edica e ha we s eng hen o de elop a
ecognize o well- o med o mulas.
Bo olean cons an s,
nil
and
, a e ecognized by he
Acl2
booleanp
p edi-
ca e. The se o p oposi ional a iables could b e hen ep esen ed by he se o
a oms no including he Bo olean cons an s. Howe e , i we ep esen a iables
using na u al numb e s hen i is easie o sha e he same no ion o a iable in
o mulas and p olynomials. Thus, we dene ou a iable ecognize ,
a iablep
,
o ecognize jus na u al numb e s.
Ou no ion o IF-cons is cap u ed byan
Acl2
s uc u e. An IF-cons is jus
a collec ion o h ee ob jec s ( he
es
, and he
hen
and
else
b anches). The
p edica e
i -consp
will ecognize e ms cons uc ed wi h
i -cons
,while he
unc ions
es
,
hen
and
else
ac as des uc o s. Well- o med IF- o mulas can
b e ecognized by he ollowing o al ecu si e
Acl2
p edica e:
(de un o mulap ( )
(o (booleanp ) ( a iablep )
(and (i -consp )
( o mulap ( es ))
( o mulap ( hen ))
( o mulap (else )))))
An assignmen o alues o a iables can be ep esen ed as a lis o Booleans.
3
Thus, he alue o a a iable wi h espec o an assignmen is gi en by he
elemen which occupies i s co esp onding p osi ion.
(de un u h- alue ( a)
(n h a))
3
Remembe each Bo olean a iable is ep esen ed as a na u al numbe .
The alue o a o mula unde an assignmen is dened ecu si ely by he
ollowing unc ion. To make he alua ion unc ion o al, we assign an a bi a y
meaning o non- o mulas.
(de un alue ( a)
(cond ((booleanp ) )
(( a iablep ) ( u h- alue a))
((i -consp )
(i ( alue ( es ) a)
( alue ( hen ) a)
( alue (else ) a)))
( nil))) ; o comple eness
The ollowing heo em s a es a simple bu imp o an p op e y.I says ha
he alue o a o mula unde an assignmen is ue i and only i he alue o he
nega ion o ha o mula unde he same assignmen is alse. Why his p op e y
is imp o an will become clea in Sec . 4.
(de hm duali y
(implies (and ( o mulap ) (assignmen p a))
(i (equal ( alue a) )
(equal ( alue (i -cons nil ) a) nil))))
2.2 Bo olean Polynomials
In o de o ep esen p olynomials wi h Bo olean co ecien s, we can use he
Bo olean ing gi en by
{0,1},⊕,∧,0,1
whe e
⊕
is he logical exclusi e dis-
junc ion (exclusi e-o ),
∧
is he logical conjunc ion and
0
and
1
a e ega ded as
u h- alues ( alse and ue). In he ollowing deni ions, le
B={0,1}
and
¬
,
∨
s and o logical nega ion and logical disjunc ion, esp ec i ely.
Al hough i suces wi h a p olynomial Bo olean ing o ou cu en pu p oses,
whe e monomials do no need co ecien s, weha e implemen ed monomials wi h
co ecien s and e ms o euse pa o a p e ious wo k on p olynomial ings [19].
Deni ion 1.
ABoolean e m on a ni e se
V={ 1,...,
n}
o Boolean a i-
ables wi h an o de ing ela ion
<V={( i,
j):1≤i<j≤n}
is a ni e p oduc
o he o m:
n

i=1
( i∨¬ai)∀ia
i∈B.
(1)
We ob ain a qui e simple ep esen a ion o a Bo olean e m on a gi en se o
a iables by using he Bo olean sequence
a1,...,a
n
, namely,
i
app ea s in he
e m i and only i
ai=1
. The main esul s ha weha ep o ed in
Acl2
on ou
Bo olean e m o maliza ion may b e summed up in he ollowing poin s:
1. Bo olean e ms o m a commu a i e monoid wi h esp ec o a sui able mul-
iplica ion ope a ion.
2. Lexicog aphical o de ing on e ms is well- ounded.
As we usually wo k wi h Bo olean e ms dened on he same se o a i-
ables, hei sequences will ha e he same leng h. In his case hey a e said o b e
compa ible
.
Deni ion 2.
We dene he mul iplica ion o wo compa ible e ms as he ol-
lowing ope a ion:
n

i=1
( i∨¬ai)·
n

i=1
( i∨¬bi)=
n

i=1
( i∨¬(ai∨bi)) .
(2)
Ha ing chosen he se o a iables, i suces o o  hei sequences elemen
by elemen o compu e he mul iplica ion o wo compa ible e ms. A p o o
o e ms ha ing a commu a i e monoid s uc u e wi h esp ec o he p e ious
op e a ion is easily ob ained.
To o de e ms i is only necessa y o ake in o accoun hei asso cia ed
sequences. The ob ious choice is o se up a
lexicog aphical o de ing
among
hem. In he case o compa ible e ms, his deni ion is s aigh o wa d, since
he sequences in ol ed ha e he same leng h.
Deni ion 3.
The lexicog aphical o de ing on compa ible Boolean e ms is de-
ned as he ol lowing ela ion:
a1,...,a
n<b1,...,b
n≡∃i(¬ai∧bi∧∀j<ia
j=bj).
(3)
Deni ion 4.
ABoolean monomial on
V
is he p oduc o a Boolean coecien
andaBoolean e m.
c∧
n

i=1
( i∨¬ai)c∈B∀ia
i∈B.
(4)
In he same way as happened o e ms, i is sui able o dene a compa ibili y
ela ion on monomials. Wesay ha wo monomials a e
compa ible
when hei
unde lying e ms a e compa ible.
Amul iplica ion op e a ion is dened and hen i is p o ed ha monomials
ha e a monoid commu a i e s uc u e wi h esp ec o i .
Due o echnical easons i is con enien o ex end compa ibili y o monomials
o p olynomials. Toachie e his we  s say ha a p olynomial is
uni o m
i all o
i s monomials a e compa ible each o he . Hence o h, we will assume uni o mi y.
Deni ion 5.
ABoolean polynomial on
V
is a ni e sum o monomials.
m

i=1

ci∧
n

j=1
( j∨¬aij )
∀i, j ci,a
ij ∈B.
(5)
Now, he deni ion o compa ibili ybe ween p olynomials a ises in a na u al
way.Two p olynomials a e
compa ible
i hei monomials a e compa ible o o.
Finally,weha e p o ed ha Bo olean p olynomials ha e a ing s uc u e. To
achie e his, only co ecien s and e ms had o b e changed om he o maliza ion
desc ib ed in [19]. These changes a e ep o ed in [20].

2.3 In e p e a ion P ese ing T ansla ion
Nex , we use he ela ion b e ween Boolean ings and Bo olean algeb as o de i e
he ansla ion algo i hm. Le us conside a Bo olean algeb a and he ollowing
h ee place Bo olean unc ion
i
, dened on i :
∀a, b, c ∈Bi (a, b, c)=(a∧b)∨(¬a∧c).
(6)
We can build an asso cia ed
i
unc ion in he co esp onding Bo olean ing:
i (a, b, c)=a·b·(a+1)·c+a·b+(a+1)·c=a·b+a·c+c.
The ollowing
Acl2
unc ions use his o compu e he p olynomial asso ci-
a ed o a o mula (S one p olynomial). The unc ion
a iable->polynomial
ans o ms a p op osi ional a iable in o a sui able p olynomial. The unde lying
p olynomial Bo olean ing is ep esen ed by

polynomialp
,
+
,
*
,
null
,
iden i y

.
The a gumen o he unc ion
iden i y
isa echnical de ail ha gua an ees he
uni o mi y o he esul ing p olynomial.
(de un s one ( )
(s one-aux (max- a iable )))
(de un s one-aux ( n)
(cond ((booleanp ) (i (iden i y (LISP::+ n 1)) (null)))
(( a iablep ) ( a iable->polynomial n))
((i -consp )
(le ((s- es (s one-aux ( es ) n))
(s- hen (s one-aux ( hen ) n))
(s-else (s one-aux (else ) n)))
(+ (* s- es (+ s- hen s-else)) s-else)))
( (null)))) ; o comple eness
Then, a unc ion,
e
, oe alua e a p olynomial wi h esp ec o an assignmen
is dened. Finally,i isp o ed ha he ansla ion o o mulas in o p olynomials
p ese es he in e p e a ion:
(de hm in e p e a ion-p ese ing- ansla io n
(implies (and ( o mulap ) (assignmen p a))
(i ( alue a) (e (s one ) a))))
The ha d pa o he wo k is dealing wi h he heo ems ab ou he e alua ion
unc ion and p olynomial op e a ions.
3 No maliza ion
In his sec ion, we e iew he Hsiang's Canonical TRS and de elop a s aigh -
o wa d no maliza ion p o cedu e o Bo olean p olynomials. Unlike disjunc i e
and conjunc i e no mal o ms, p olynomial no maliza ion allows us o associa e
a unique p olynomial o each P oposi ional Logic Fo mula.
3.1 Hsiang's Canonical TRS o Bo olean Algeb as
A Bo olean ing wi h iden i y
B,+,·,0,1
isa ing ha is idemp o en wi h
esp ec o
·
.I isaknown ac ha e e y Bo olean ing is nilpo en wi h espec o
+
and commu a i e. Hsiang [11,12] de i es his canonical e m- ew i ing sys em
o Bo olean algeb as by  s gene a ing a canonical sys em o Bo olean ings.
Fi s ly, he conside s he Bo olean ing axioms:
4
A1.
a+(b+c)=(a+b)+c
(asso cia i i yo
+
).
A2.
a+b=b+a
(commu a i i yo
+
).
A3.
a+0=a
( igh iden i yo
+
).
A4.
a+(−a)=0
( igh in e se o
+
).
A5.
(a·b)·c=a·(b·c)
(asso cia i i yo
·
).
A6.
a·(b+c)=a·b+a·c
(dis ibu i i yo
·
o e
+
).
A7.
a·1=a
( igh iden i yo
·
).
A8.
a·a=a
(idemp o ency o
·
).
T1.
a+a=0
(nilp o ency o
+
).
T2.
a·b=b·a
(commu a i i yo
·
).
By execu ing he AC-comple ion p o cedu e on hese ules, he ob ains he
BR canonical TRS o Bo olean ings. Then, BR can b e comple ed
5
by adding
ules o ans o ming he usual Boolean algeb aic op e a ions in o Bo olean ing
op e a ions, ob aining he BA canonical TRS o Boolean algeb as.
BR: BA:
a+0−→ a,
a·(b+c)−→ a·b+a·c,
a·0−→ 0,
a·1−→ a,
a·a−→ a,
a+a−→ 0,
−a−→ a.
a∨b−→ a·b+a+b,
a∧b−→ a·b,
¬a−→ a+1,
a=⇒b−→ a·b+a+1,
a⇐⇒ b−→ a·b·1,
a+0−→ a,
a·(b+c)−→ a·b+a·c,
a·0−→ 0,
a·1−→ a,
a·a−→ a,
a+a−→ 0.
4
No e ha , T1 and T2 a e no axioms, bu heo ems ha a e added so ha he
AC-unica ion algo i hm can b e used.
5
The
−a−→ a
ule is disca ded since he in e se o
+
has no signican meaning in
Bo olean algeb as.
The e o e, he i educible o m o any Boolean algeb a e m is he no mal
exp ession dened by he BA TRS ab o e, and i is unique (since BA is a canonical
TRS). This implies ha a o mula om P op osi ional Logic is a au ology i and
only i i s i educible exp ession is
1
, and i is a con adic ion i and only i i s
i educible exp ession is
0
.
3.2 A S aigh o wa d No maliza ion Algo i hm
An algo i hm can be de elop ed o a oid he o e head asso cia ed o Hsiang's
TRS. Ins ead o ew i ing mo dulo BA, o mulas a e ansla ed o p olynomials
and hen p olynomial no maliza ion is used. Once weha e dened an o de on
e ms, we can say ha a p olynomial is in no mal o m i and only i hei
monomials a e s ic ly o de ed by he dec easing e m o de and none o hem is
null. This deni ion implies he absence o iden ical monomials in a no malized
uni o m p olynomial. We di ide he sp ecica ion o he no maliza ion unc ion
in wo s eps:
1. A unc ion capable o adding a monomial o a polynomial. This mus b e a
no maliza ion-p ese ing unc ion.
2. A no maliza ion unc ion s able o no malized null polynomials ha adds
he  s monomial o he no maliza ion o he emaining monomials by using
he p e ious unc ion.
The no maliza ion unc ion is easy o dene: i he p olynomial is null, i
is al eady in no mal o m, o he wise, i suces o no malize he es o he
p olynomial and hen add he  s monomial o he esul .
(de un n (p)
(cond ((o (no (polynomialp p)) (nullp p)) (null))
( (+-monomial ( i s p) (n ( es p))))))
In o de o make
+-monomial
o al we need o comple e, aking he u mos
ca e, he alues ha i e u ns when i is no applied o a p olynomial.
Nex , we show he mos imp o an pa o he deni ion o
+-monomial
unc ion. I akes a monomial
m
and a p olynomial
p
as i s a gumen s.
1. I
m
is null,
p
is e u ned.
2. I
p
is null, he p olynomial composed o
m
is e u ned.
3. I
m
and he  s monomial o
p
ha e he same e m, bo h monomials a e
added. I he esul is null hen he es o
p
is e u ned, o he wise a poly-
nomial consis ing o he esul ing monomial and he es o
p
is e u ned.
4. I
m
is g ea e han he  s monomial o
p
, a p olynomial consis ing o
m
and
p
is e u ned.
5. O he wise, a p olynomial consis ing o he  s monomial o
p
and he esul
o ecu si ely adding
m
o he es o
p
is e u ned.
Imp o an p op e ies o he no maliza ion unc ion ha e been p o ed, such
as ha i mee s i s sp ecica ion,
(de un n p (p)
(equal (n p) p))
(de hm n p-n
(n p (n p)))
and ha p olynomial uni o mi y is p ese ed unde no maliza ion.
(de un uni o mp (p)
(o (nullp p) (nullp ( es p))
(and (MON::compa iblep ( i s p) ( i s ( es p)))
(uni o mp ( es p)))))
(de hm uni o mp-n
(implies (uni o mp p)
(uni o mp (n p))))
One ele an esul s a es ha he no mal o m o a polynomial is s ic ly
dec easingly o de ed wi h esp ec o he lexicog aphical o de dened on e ms.
(de hm o de edp-n
(o de edp (n p)))
In o de o ob ain his, we dene he unc ion
o de edp
by using he lexico-
g aphical o de dened on e ms.
(de un e m-g ea e - han-leade (m p)
(o (nullp p) (TER::< (MON:: e m ( i s p)) (MON:: e m m))))
(de un o de edp (p)
(and (polynomialp p)
(o (nullp p)
(and (no (MON::nullp ( i s p)))
( e m-g ea e - han-leade ( i s p) ( es p))
(o de edp ( es p))))))
4 A Decision P o cedu e
In his sec ion, ou main aim is o cons uc a p olynomial-based p o cedu e o
deciding whe he a p oposi ional logic o mula is a au ology and p o e i s co -
ec ness.
A o mula is a au ology i and only i he alue o he o mula unde e e y
p ossible assignmen o alues o a iables is ue. So, he ollowing  s -o de
o mula s a es he co ec ness o a au ology-checke :
∀ [
( au ology-checke
)
⇐⇒ ∀ a
( alue
a
)
=
]
(7)
Howe e , i is no p ossible o w i e di ec ly his heo em in
Acl2
, due o he
lacko quan ie s. Fo example, he ollowing  heo em do es no cap u e ou
idea:
9. Ha ison, J.: Bina y Decision Diag ams as a HOL De i ed Rule. The Compu e
Jou nal
38
(1995)
10. Ha ison, J.: S ªma ck's Algo i hm as a HOL De i ed Rule. 9 h In e na ional
Con e ence on Theo em P o ing in Highe O de Logics. LNCS
1125
(1996)
11. Hsiang, J.: Re u a ional Theo em P o ing using Te m-Rew i ing Sys ems. A i-
cial In elligence
25
(1985)
12. Hsiang, J.: Rew i e Me ho d o Theo em P o ing in Fi s -O de Theo y wi h
Equali y. J. Symbolic Compu a ion
3
(1987)
13. Hsiang, J., Huang, G. S.: Some Fundamen al P op e ies o Bo olean Ring No mal
Fo ms. DIMACS se ies on Disc e e Ma hema ics and Compu e Science: The
Sa isabili y P oblem. AMS (1996)
14. Kau mann, M., Mo o e, J S.: An Indus ial S eng h Theo em P o e o a Logic
Based on Common Lisp. IEEE T ans. on So wa e Enginee ing
23
(4) (1997)
15. Kau mann, M., Manolios, P., Mo o e, J S.: Compu e -Aided Reasoning: An Ap-
p oach. Kluwe Academic Publishe s (2000)
16. Kau mann, M., Manolios, P., Mo o e, J S.: Compu e -Aided Reasoning: ACL2 Case
S udies. Kluwe Academic Publishe s (2000)
17. Kapu , D., Na end an, P.: An Equa ional App oach o Theo em P o ing in Fi s -
O de P edica e Calculus. 9 h In e na ional Con e ence on A icial In elligence
(1985)
18. Lai a, L. M., Roanes-Lozano, E., Ledesma, L., Alonso, J. A.: A Compu e Algeb a
App oach oVe ica ion and Deduc ion in Many-Valued Knowledge Sys ems. So
Compu ing
3
(1) (1999)
19. Medina-Bulo, I., Alonso-Jiménez, J. A., Palomo-Lozano, F.: Au oma ic Ve ica ion
o Polynomial Rings Fundamen al P ope ies in ACL2. ACL2 Wo kshop 2000
P o ceedings, Pa A. The Uni e si yo Texas a Aus in, Depa men o Compu e
Sciences. Technical Rep o TR0029 (2000)
20. Medina-Bulo, I., Palomo-Lozano, F., Alonso-Jiménez, J. A.: A Ce ied Algo i hm
o T ansla ing Fo mulas in o Polynomials. An ACL2 App oach. In e na ional
Join Con e ence on Au oma ed Reasoning (2001)
21. Mo o e, J S.: In o duc ion o he OBDD Algo i hm o he ATP Communi y.
Compu a ional Logic, Inc. Technical Rep o 84 (1992)
22. Paulin-Moh ing, C., We ne , B.: Syn hesis o ML P og ams in he Sys em Co q.
J. Symb olic Compu a ion
15
(56) (1993)
23. S one, M.: The Theo y o Rep esen a ion o Boolean Algeb a. T ans. AMS
40
(1936)
24. Sumne s, R.: Co ec ness P o o o a BDD Manage in he Con ex o Sa isabili y
Checking. ACL2 Wo kshop 2000 P o ceedings, Pa A. The Uni e si yo Texas a
Aus in, Depa men o Compu e Sciences. Technical Rep o TR0029 (2000)
25. Thé y,L. AMachine-Checked Implemen a ion o Buchb e ge 's Algo i hm. J. Au-
oma ed Reasoning
26
(2001)
26. Wu, J., Tan, H.: An Algeb aic Me ho d o Decide he Deduc ion P oblem in P op o-
si ional Many-Valued Logics. In e na ional Symp osium on Mul iple-Valued Logics.
IEEE Compu e So cie y P ess (1994)
27. Wu, J.: Fi s -O de Polynomial Based Theo em P o ing. In: Gao, X., Wang, D.
(eds.): Ma hema ics Mechaniza ion and Applica ions. Academic P ess (1999)
28. Zhang, H.: A New S a egy o he Bo olean Ring Based App oach o Fi s O de
Theo em P o ing. Depa men o Compu e Science. Uni e si yo Iowa. Technical
Rep o (1991)
29. Zhegalkin, I. I.: OnaTechnique o E alua ion o P op osi ions in Symb olic Logic.
Ma . Sb.
34
(1927)