数理解析研究所講究録
第 666 巻 1988 年 29-40$v$

Boolean Gr\"obner Bases
K\^o Sakai and Yosuke Sato

ICOT Research Center
1-4-28, Mita, Minato-ku, Tokyo 108, JAPAN(April 8, 1988)

ABSTRACTThis paper proposes an algebraic tool to solve the constraints ofpropositional calculus. Any constraint of propositional calculus canbe described in terms of equations in a Boolean algebra, and alsotranslated into equations of a Boolean ring where the constraint isrepresented in the form of a finite set of polynomials. We give analgorithm which produces a rewriting system for a given Boolean
constraint, which reduces Boolean polynomials equivalent under theconstraint to the same normal form. The algorithm is a central partof the constraint solver in CAL (Contrainte avec Logique), which isa constraint logic programming language being developed at ICOT.
1. Boolean ring

We assume that the reader is familiar with elementary algebraic notions such as ringand ideal (see [Waerden 37, 40], for example), and the terminology of rewriting systems(see [Huet 80], for example).
$\neg>$ , define $x+y=def(x\wedge\neg y)\vee(\neg x\Lambda y)$ andFor a Boolean algebra $<B,$$B$$x\cross y=defx\wedge y$ for eachin , then $<B,$ $+>is$ known to be a commutative
ring with a unit with the following properties.
$\vee,$$x,$(i)$\forall x\in B$$x+x=0$(ii)$\forall x\in B$$x\cross x=x$$\wedge,$$y$$\cross,$

A ring with these properties is called a Boolean ring. Here, we define a Boolean ringof polynomials specifically, as used in this paper

Definition 1.1
Let there be countably many Boolean variables, which are denoted by metasymbols. A Boolean monomial is a (finite) multiset of Boolean variables. It is denotedby $using\cross$ . For example,
denotes multiset $\{a, a, b, c\}$ . The empty Boolean$a,$ $b,$ $c,$ $\ldots$$a\cross a\cross b\cross c$$rightarrow\iota-$

$\delta U$

for Boolean mononials.
monomial, , is denoted 1. We use metasymbols $A,$ $B,$ $C,$$B$ .
$A\cross B$ is defined as the multiset union ofandFor example, $A\cross B=\{a, a, b, c\}$
$B=\{a,c\}$. A Boolean polynomial is a (finite) multiset of Boolean
when $A=\{a, b\}$ and$using+$by. For example, $A+A+B+C$ denotes multisetismonomials. It denoted$\{A, A, B, C\}$ . The empty Boolean polynomial,, is denoted . We use metasymbols$X,$ $Y,$ $Z,$
for Boolean polynomials. $X+Y$ is defined as the multiset union of X
extended to Boolean polynomials in a natural way. For
and Y. Binary function
example,$\{\}$$\ldots$$A$$0$$\{\}$$\ldots$$\cross is$$(A+B)\cross(A+C+D)=A\cross A+A\cross C+A\cross D+B\cross A+B\cross C+B\cross D$ .

Note that both $\cross and+are$ associative and commutative, and are also distributive,i.e., $X\cross(Y+Z)=X\cross Y+X\cross Z$ for each Boolean polynomial, $X,$ , and .
andto denote Boolean monomials
We abuse metasymbols$\{B\},$$A,$ $B,$ $C,$$\{C\},$$\{A\},$, which will be clear from thefor Boolean polynomials
context.
$Z$

$Y$

$a,$

$b,$ $c,$$\{a\},$ $\{b\},$ $\{c\},$ $\ldots$$\ldots$$\ldots$$\ldots$

In this paper, we omit$\cross$. For example, we write $aab$ instead of$a\cross a\cross b$.

Definition 1.2, on Boolean monomials is defined as $X+aaAarrow\cross X+aA$ for
The rewriting rule,o\’{n} Boolean
each variable , monomial , and polynomial $X$ . The rewriting rule,polynomials is defined as $X+A+Aarrow+X$ for each monomial and polynomial $X$ .
$arrow\cross$

$A$

$a$

$arrow+$$A$

It is easy to show the following:
Proposition 1.3
The rewriting system of rules$\{arrow\cross, arrow_{+}\}$

is confluent and terminating.

1

Definition 1.4
is denoted
For a Boolean polynomial, $X$ , the normal form of $X$ by$aabbccc\downarrow=abc,$$(aabc+abcc+$
and called a Boolean normal polynomial. For example,$bc+cdd)\downarrow=bc+cd$ . A Boolean normal polynomial is the sum of different Boolean
monomials, each of which is the product of different Boolean variables.
$\{arrow\cross, arrow_{+}\}$$X\downarrow$

Definition 1.5
Define the product,$\cross$, and the sum,$+$, of Boolean normal polynomials as follows:$(X\downarrow)\cross(Y\downarrow)=def(X\cross Y)\downarrow$$(X\downarrow)+(Y\downarrow)=def(X+Y)\downarrow$

It is easy to check that these are well-defined.
The set of all Boolean normal polynomials with operations $\cross and+$ , defined above,
forms a Boolean ring.

–2–

31

2. Boolean Grobner baseDefinition 2.1
Let $\geq be$ an ordering on Boolean monomials. The ordering is said to be admissible if
the following hold:(i)for any monomials
inclusion.

(ii)

If $A\geq B$ , then $AC\geq BC$ for any monomials $A,$

$A\geq B$$A$

and $B$ such that

$A\subseteq B$

$B$

, and

in the sense of multiset$C$.

Let be a fixed finite set of Boolean variables. The fact that an admissible ordering
is well-founded is well known as
on monomials consisting only of the variables inDickson’s lemma [Dickson 13], or easily proven as its corollary. An admissible orderingon monomials is extended to polynomials by employing induced multiset ordering[Dershowitz 79]. Since induced multiset ordering is well-founded if the base ordering
is well-founded, the extension is well-founded on polynomials consisting only of thevariables in . Moreover, induced multiset ordering is total if the base ordering is total.
In what follows let $\geq be$ a fixed admissible total ordering on Boolean monomials.
$V$

$V$

$V$

Definition 2.2

is the greatest Boolean
Let $A+X$ be a Boolean normal polynomial such that$Y$
be a Boolean polynomial such thatmonomial in $A+X$ with respect to . Let
polynomial
such that $V=T+AC$ . If isanda
Booleannormalbe$Y=S+AB$a Boolean polynomial such that $Z=S+XB$ and $W$ is a Boolean normal polynomial
such that $W=(T+XC)\downarrow$ , then we write $Yarrow A+xZ$ and $V\Rightarrow A+xW$ .
$A$$\geq$$Z$$V$

This means that or $W$ is obtained from or by substituting
the rule $A=X$ which is equivalent to $A+X=0$ .
$Y$

$Z$

$V$

$A$

for $X$ by using

is the biggest Boolean monomial in any Boolean
In this paper, we assume that
such
as $A+X$ .
expressions
normal polynomial$A$

Example 2.3
Let $Y=abc+bc$ . Then $Yarrow_{ab+c}cc+bc$ and $Y\Rightarrow_{ab+c}c+bc$ , since $(cc+bc)\downarrow=c+bc$ .

Lemma 2.4
Let $A+X$ be a Boolean normal polynomial. If $Yarrow A+XZ$ , then $Y>Z$ for any
Boolean polynomials and . If $V\Rightarrow A+XW$ , then $V>W$ for any Boolean normal
polynomials and $W$ .
$Z$

$Y$

$V$

Proof:

Easy to check.

1–3–

Corollary 2.5

For any set of Boolean normal polynomials $\{X_{1}, X_{2}, \ldots, X_{n}\}$ , the rewriting systems
andare terminating.
$\{arrow\cross, arrow+, arrow x_{1}, arrow x_{2}, \ldots, arrow x_{n}\}$1$\{\Rightarrow x_{1}, \Rightarrow x_{2}, \ldots, \Rightarrow x_{n}\}$Definition 2.6
be a finite set of Boolean normal polynomials. We write
if there exists$X\in R$ such that $Y\Rightarrow xZ$ , and $Y4_{R}Z$ if $Y=Z$ or there exists a possibly empty
sequenceof polynomials such that
. That isis the transitive reflexive closure
.

Let

$R$

$Y\Rightarrow_{R}Z$$Y_{1},$$Y_{2},$$\ldots,$$Y_{m}$$Y\Rightarrow_{R}Y_{1},$ $Y_{1}\Rightarrow_{R}Y_{2},$$\xi_{R}$$Y_{m},$ $Y_{m}\Rightarrow_{R}Z$$\ldots,$$Y_{m-1}\Rightarrow R$$of\Rightarrow R$

In what follows, we will discuss ideals in the ring of Boolean normal polynomials.
Intuitively, an ideal can be regarded as the set of all normal polynomials of value
under a certain constraint.

$0$

Definition 2.7
Let be an ideal of the ring of Boolean normal polynomials. A Grobner base for is a
finite set of Boolean normal polynomials $R$ suchis confluent and terminating,and moreover, the following two conditions are equivalent for any polynomials, $X$ and
Y.
$I$

$I$

$that\Rightarrow R$(i)$(X+Y)\downarrow\in I$(ii)

There exists a polynomial,(or $X\equiv Y(mod I)$ )$Z$, such that

$X\Rightarrow_{R}Z$

and$Y\Rightarrow_{R}Z$.

Theorem 2.8
Let $E$ be an arbitrary finite set of Boolean normal polynomials, then a Gr\"obner basefor the ideal generated by $E$ exists and, furthermore, we have an algorithm to construct
it from $E$ .
Intuitively, an element of the generated ideal is a polynomial of value under theconstraint that all elements in $E$ have value . A Gr\"obner base can be viewed as amechanism to determine whether a certain polynomial is in the ideal. First, we givean algorithm, then show its correctness. We need to define several notions.
$0$

$0$

Definition 2.9

Let be a finite set of Boolean normal polynomials. For each Boolean normal polynomial $X,$
denotes a Boolean normal polynomial, , such thatand $Y$i.e., there exists no Boolean normal polynomial, , such thatis irreducible
Z. (Note that Corollary 2.5 assures the existence of such Y. However, it may
not be unique.
denotes one Y.)
$R$

$Y$

$X\downarrow R$$X\Rightarrow_{R}Y$$Z$$by\Rightarrow R$$Y\Rightarrow R$$X\downarrow R$

–4–

33

Definition 2.10
Let $A+X$ be a Boolean normal polynomial, and$a$a variable in$A$. Then $(aX+X)\downarrow$is called a self-critical pair of $A+X$ .

If $A+X$ is in an ideal, , then so are all the self-critical pairs of $A+X$ . In fact,$I$

let $a\in A$ , i.e., $A=aB$ for some (possibly empty) Boolean monomial, $B$ . Then,$aB+X\in I$ implies $((a+1)(aB+X))\downarrow=(aX+X)\downarrow\in I$ .

Example 2.11

Let $A+X$ be $ab+b+c$ . Then, $(a(b+c)+(b+c))\downarrow=ab+ac+b+c$ and $(b(b+c)+(b+c))\downarrow=$$bc+c$. Therefore, self-critical pairs of $A+X$ are $ab+ac+b+c$ and $bc+c$ .

Definition 2.12
Let $A+X$ and $B+Y$ be Boolean normal polynomials, and$C$

the intersection of$A$

and as multisets. According to tradition, let us call the GCD (greatest common
divisor) of and . Suppose that $A=CA’$ and $B=CB’$ . Then, $(B’X+A’Y)\downarrow is$
$C$

$B$

$A$

$B$

called the critical pair between $A+X$ and $B+Y$ .
If $A+X$ and $B+Y$ are in an ideal, , then so is the critical pair between $A+X$ and$I$$B+Y$ . In fact, $(B’(A+X)+A’(B+Y))\downarrow=(- B’X+A’Y)\downarrow\in I$ .

Example 2.13
Let $A+X=abc+a+b$ and $B+Y=abd+a+b$ , then $(d(a+b)+c(a+b))\downarrow=$$ac+ad+bc+bd$ . Therefore, $ac+ad+bc+bd$ is the critical pair between $abc+a+b$

and $abd+a+b$ .

Definition 2.14

Let $X$ be a Boolean normal polynomial and$R$

be a finite set of Boolean normal

polynomials, then $CP(X, R)$ denotes the set consisting of all the non-zero criticalpairs between $X$ and each element of $R$ and all the self-critical pairs of $X$ .

–5–

Now the algorithm can be presented.

input $E$
$Rarrow\emptyset$

while $E\neq 0$choose $X\in E$$Earrow E-\{X\}$ and $X’arrow X\downarrow R$

if $X’\neq 0$ thenfor every $A+Y\in R$
ifthen $Earrow E\cup\{(Z+Y)\downarrow\}$ and $Rarrow R-\{A+Y\}$
else $Rarrow(R-\{A+Y\})\cup\{A+Y\downarrow_{R\cup\{X’\}}\}$
end-ifend-for$Earrow E\cup CP(X’, R)$ and $Rarrow R\cup\{X’\}$end-ifend-while
output( is a Gr\"obner base)$A\Rightarrow_{X’}Z$

$R$

$R$

(In this algorithm, the choice of an element in $E$ should be fair. That is, any elementof $E$ should be chosen at some stage in the outermost while loop.)

This algorithm terminates and returns a Gr\"obner base. To prove the correctness of
the algorithm, we study a more general form of the algorithm.
Definition 2.15

We define inference rules on pairs $(E, R)$ of finite sets of Boolean normal polynomials.

Rule 1

Rule 2Rule 3Rule 4$E\cup\{X\},$ $R$

where$E\cup\{Y\},$ $R$$X\Rightarrow_{R}Y$$\frac{E\cup\{0\},R}{E,R}$$E,$ $R\cup\{A+X\}$$E,$ $R\cup\{A+Y\}$$\frac{E,R\cup\{AB+X\}}{E\cup\{(AZ+X)\downarrow\},R}$

where$X\Rightarrow_{R}Y$

where $B+Z\in R$ and–6–$A\neq\emptyset$

35$E\cup\{A+X\},$ $R$

Rule 5$E,$ $R\cup\{A+X\}$

Rule 6$\frac{E,R}{E\cup\{(CX+BY)\downarrow\},R}$

Rule 7

where $AB+X,$ $AC+Y\in R$ and $B\cap C=\emptyset$

where $aA+X\in R$$\frac{E,R}{E\cup\{(aX+X)\downarrow\},R}$

Definition 2.16

(critical pair)(self-critical pair)(General form of the algorithm). For each , let
be obtained from
andby oneLet $E_{0}=E,$
andis denoted byof the above rules. In the following,and. We give priority to Rules 1 and 2. We need two restrictions to make thebyalgorithm correct.
$R_{0}=\emptyset$$i$$R_{i+1}$$E_{i+1}$$E_{i}$$E^{\infty}$$\bigcup_{n=1}^{\infty}\bigcap_{i=n}^{\infty}E_{i}$$R_{i}$$\bigcup_{n=1}^{\infty}\bigcap_{i=n}^{\infty}R_{i}$$R^{\infty}$(i)

The algorithm must be fair, i.e.,$E^{\infty}=\emptyset$.

(ii) Any possible critical pair or self-critical pair must be taken, i.e., for each $X\in$, any self-critical pair of $X$ must be put in someby Rule 7 and for each$X,$, any critical pair of $X$ and must be put in someby Rule 6.
$R^{\infty}$$E_{i}$$Y$$Y\in R^{\infty}$$E_{i}$

is empty andis a Gr\"obner base. (Note that the previous
Then for somealgorithm takes the form defined here.)$i,$$E_{i}$$R_{i}$

To prove the last statement, we need some more definitions.

Definition 2.17
be a finite set of Boolean normal polynomials. A rewriting rule on Boolean$polynomialarrow R$ is defined as follows. $Xarrow_{R}Y$ iff $Xarrow zY$ for some $Z\in R$ .
isdefined as a reflexive and transitive closure ofandas a symmetric,$ofarrowR$.
reflexive and transitive closure

Let

$R$

$arrow R*$$\{arrow R, arrow\cross, arrow_{+}\}$$rightarrow R*$

Definition 2.18
Let $X$ and be arbitrary Boolean polynomials such that $Xarrow A+zY$ for $A+Z\in E_{i}$ .
We associate the rewriting $Xarrow A+zY$ with a triple $(\{X, X\}, A, Z)$ , where {X, $X$ } isa multiset. Similarly, we associate the rewriting $Xarrow A+ZY$ for $A+Z\in R_{i}$ with atriple $(\{X\}, A, Z)$ . We also associate the rewriting $Xarrow\cross Y$ or $Xarrow+Y$ with a triple$(\{X\}$ ,, , where is a special constant. We introduce an ordering on the above
triples defined as follows. The first component is compared by the multiset ordering
induced by the ordering on Boolean polynomials and the second or third component
is compared as a Boolean monomial or Boolean normal polynomial, respectively. We$Y$$\bullet$$\bullet$$)$$\bullet$–7–define as bigger than any Boolean monomial and any Boolean normal polynomial.
Finally, we define an ordering on triple lexicographically by the components. We
denote this ordering . Note that this is well-founded. We also consider this ordering
as an ordering on rewritings.
$\bullet$$\geq$

Definition 2.19
is a sequence
Let $X$ and $Y$ be arbitrary Boolean polynomials. A proof ofis a rewriting fromto $X_{J+1}$ orof rewritings such that eachfrom $X_{j+1}$ towhere $X_{0}=X$ and $X_{m}=Y$ . Note that there might be many
proofs ofin general. We define an ordering on proofs as the multiset
ordering induced by the ordering on rewritings defined above. Note that this is also
well-founded.
$X^{*}rightarrow E_{1}\cup R;Y$$\Xi_{1},$ $\Xi_{2},$$\Xi_{m}$$X_{j}$$\Xi_{j}$$\ldots,$$X_{j}$$X^{*}rightarrow E:\cup R:Y$

Note that the definition of the ordering does not depend on . Therefore, we can, even if and are different.
compare a proof ofand a proof of$i$$X^{*}rightarrow E:\cup R:Y$$i$

$X^{*}rightarrow E_{j}\cup R_{j}Y$$j$Lemma 2.20

, is the same for every . Moreover, if a proof, , ofThe equivalence relation,for each $j>i$ suchis given, we can construct a proof, , of.
that$\Psi$$i$$rightarrow E;\cup R_{i}*$$X^{*}rightarrow E:\cup R;Y$$\Phi$$X^{*}rightarrow E_{j}\cup R_{j}Y$$\Psi\geq\Phi$

Proof:(i)

It is enough to show the following.

If a proof,$X^{*}rightarrow E_{i}\cup R:Y$(ii) If a proof,$\Phi$, of$X^{*}rightarrow E_{i+1}\cup R_{i+1}Y$

is given, we can construct a proof,$\Psi$, of.
$\Psi$, of$X^{*}rightarrow E_{i+1}\cup R:+1Y$$X^{*}rightarrow E:\cup R:Y$

such that$\Psi\geq\Phi$

is given, we can construct a $pro$ of,.

$\Phi$, of, for $X$ , which is a new Boolean
The first claim is shown by checking that the rule,normal polynomial added to $E_{i+1}UR_{i+1}$ by Rule 1-8, can be simulated by a combi. The second claim is shown similarly, but
nation $ofarrow\cross’arrow+and$ the rules inin this case it must be verified that the simulation generates the same proof or lessthan it. Later, we will show such simulation in several interesting cases. However,since such simulation is a routine in general, we omit details.
$arrow x$$E_{i}\cup R_{i}$1on Boolean polynomials.
(We have this property since we discussed a rewriting rule,normal polynomials.)
Note that this property does not hold$arrow$$for\Rightarrow on$

We use the simple notation,
does not depend on .

$rightarrow*$for the above equivalence relation,$i$

Before going to the next step, we will show several lemmata.

–8–$rightarrow E_{i}\cup R_{i}*$, since it

37Lemma 2.21
Let be a monomial andsuch that
simply$A$$U$$X_{1},$$X_{2}$, andand$Z+AX_{1^{arrow}(X_{1}+X_{2})\downarrow}^{*}U$$Z$

polynomials. Then there exists a polynomial. We denote this situation$Z+AX_{2^{arrow}(X_{1}+X_{2})\downarrow}^{*}U$$Z+AX_{1^{arrow(X_{1}+X_{2})\downarrowarrow z}}^{**}+AX_{2}$Proof: If$(X_{1}+X_{2})\downarrow=0$, clearly$X_{1}\downarrow=X_{2}\downarrow$.

. Then,$Z+AX_{1^{arrow}}^{*}Z+A(X_{1}\downarrow)=Z+A(X_{2}\downarrow)*arrow Z+AX_{2}$,denotes application $ofarrow\cross andarrow+$ , performed a finite number of times. If$(X_{1}+X_{2})\downarrow\neq 0$ , then let $(X_{1}+X_{2})\downarrow=C+W$ , then, either.
$C\in
X_{1}$. Let $X_{1}\downarrow=C+X$ . Then,
Without loss of generality, we can assume that$wherearrow*$$C\in X_{1}\downarrow orC\in X_{2}\downarrow$$Z+AX_{1^{arrow}}^{*}Z+AX_{1}\downarrowarrow_{C+W}Z+A(W+X)arrow*Z+A((W+X)\downarrow)$$Z+AX_{2^{arrow}}^{*}Z+A(X_{2}\downarrow)$

It is clear that$(W+X)\downarrow=X_{2}\downarrow$

.

.

$1$

Lemma 2.22

orSuppose that Rule 1, 3, 4, or 5 is applied in the i-th step and a polynomial in, say $X$ , is eliminated. Any rewriting $usingarrow x$ can be replaced by a smaller proof
in $E_{i+1}\cup R_{i+1}$ .
$E_{i}$$R_{i}$The lemma is clear for Rule 5 by the definition of the ordering. We show thelemma only for Rule 4. The proof is almost the same for Rules 1 and 3, and much.
easier. Let $X=AB+X’$ for some $B,$ , and $X’$ such that $B+Z\in R_{i}$ and$P$
Then $(AZ+X’)\downarrow\in E_{i+1}$ . If $Parrow AB+x\prime Q,$ is of form $W+CAB$ and is of form
$W+CX’$ . Therefore, by the above lemma,

Proof:$A$$A\neq\emptyset$$Q$$P=W+CABarrow B+zW+CAZarrow(AZ+X’)\downarrowarrow W+CX’=Q$ .

Finally, let us verify that this proof is smaller than the original proof, $Parrow AB+X^{t}Q$ .
The first rewriting, $Parrow B+ZW+CAZ$ , is smaller, since $B<AB.$ Therefore, thewhole proof is smaller, since the other rewritings are clearly smaller. I

Lemma 2.23
Let $X$ and
.
of

$Y$

be arbitrary Boolean polynomials, and$\Xi_{1},$ $\Xi_{2},$$Xrightarrow*Y$(i) There is no rewriting in it which uses a rule in some–9–

$E_{i}$.

$\Xi_{m}$$\ldots,$a minimal proof

is a rewriting from(ii) There is no such that
to $X_{j-1}$ and
to $X_{J+1}$ (we denote this situation $X_{j-1}arrow X_{j}arrow X_{J+1}$ ).
from$\Xi_{j-1}$$j$$X_{j}$$\Xi_{j}$is a rewriting$X_{j}$

Proof of (i): Suppose some is a rewriting, $Xarrow zY$ , for in some . By conditionis eliminated at some stage, $k>j$ . By the(i) of the definition of the algorithm,
above lemma, there is a proof ofinwhich is less than. Thiscontradicts the minimality.
$Z$$\Xi_{i}$$E_{j}$$Z$$Xrightarrow*Y$$E_{k}\cup R_{k}$$\Xi_{i}$is a rewriting, $Xarrow zY$ , for in some
Proof of (ii): Also by the above lemma, if
should be in. Suppose we have $X_{j-1}arrow X_{j}arrow X_{j+1}$ . There are several
possibilities.
$Z$$\Xi_{i}$$R_{j},$$Z$$R^{\infty}$

Case 1: Both reductions $arearrow\cross orarrow+\cdot$ In this case,$X_{j-1}arrow X_{j}arrow X_{j+1}$ can be replaced by$X_{j-1}\downarrow=X_{J+1}\downarrow$$XJ^{-1^{**}}arrow X_{j-1}\downarrow=X_{j+1}\downarrowarrow X_{j+1}$. Therefore,,

which is easily verified to be less than $X_{j-1}arrow X_{j}arrow X_{j+1}$ . This contradicts theminimality.

Case 2: One reduction $isarrow\cross and$ the $otherarrow R\infty$ . We can assume. There are three subcases.

$X_{j-1}arrow\cross X_{j}arrow R\infty$$X_{j+1}$

Subcase 1: $X_{j}=P+aaA,$ $X_{j-1}=P+aA,$$Parrow R^{\infty}P’$

Subcase 2: $X_{j}=P+aaA,$ $X_{j-1}=P+aA,$$Aarrow^{R_{\infty}}S$, and $X_{j+1}=P’+aaA$, and $X_{j+1}=P+aaS$

Subcase 3: $X_{j}=P+BaaA,$ $X_{j-1}=P+BaA,$ $aA+S\in R^{\infty}$ , and $X_{J+1}=P+BaS$
We consider only Subcase 3. The others are much simpler. Since $aA+S\in R^{\infty}$ , its
self-critical pair $(aS+S)\downarrow\in E_{k}$ for some by condition (ii) of the definition of thealgorithm. Then $X_{j-1}arrow X_{j}arrow X_{J+1}$ can be replaced by$k$$X_{j-1}=P+BaAarrow aA+sP+BS*arrow(aS+S)\downarrow*arrow P+BaS=X_{j+1}$ ,which is easily verified to be less than $X_{j-1}arrow X_{j}arrow X_{i+1}$ . This contradicts theminimality.

Case 3: One reduction $isarrow+and$ theeasily.
Case 4: Both reductions$arearrow R^{\infty}$$otherarrow R^{\infty}$. This case is handled much more

. There are two subcases.

Subcase 1: $X_{j}=P+A+B,$ $Aarrow R^{\infty}S,$ $X_{j-1}=P+S+B,$ $Barrow R^{\infty}T$ , and$X_{J+1}=P+A+T$

–10–

39

Subcase 2: $X_{j}=P+DABC,$ $AB+S,$ $AC+T\in R^{\infty},$ $X_{j-1}=P+DCS$ , and$X_{j+1}=P+DBT$ where $A\cap B=\emptyset$

Subcases 1 and 2 are easy. For Subcase 3, since $AB+S,$ $AC+T\in R^{\infty}$ , their criticalpair $(CS+BT)\downarrow\in E_{k}$ for some by condition (ii) of the definition of the algorithm.
Then $X_{j-1}arrow X_{j}arrow X_{J+1}$ can be replaced by$k$$X_{j-1}=P+DCSarrow(CS+BT)\downarrowarrow P+DBT=X_{i+1}$ ,which is easily verified to be less than $X_{j-1}arrow X_{j}arrow X_{j+1}$ . This contradicts theminimality. I
Lemma 2.24

is a confluent and terminating rewriting system on
Boolean polynomials for equivalence relation$\{arrow x|X\in R^{\infty}\}\cup\{arrow*’arrow+\}$$rightarrow*$

Proof: Confluence is clear from the above lemma and its proof. Termination is

Corollary 2.5. II
Lemma 2.25

Let and be arbitrary Boolean normal polynomials such thata Boolean normal polynomial, , such that $S4_{R}\infty Z$ and $T4_{R\infty}Z$ .
$S$$S*rightarrow T$$T$, then there is$Z$

by $\{arrow x|X\in R^{\infty}\}\cup\{arrow\cross, arrow_{+}\}$ .
Let
be the normal form of andSince the rewriting system is confluent and terminating, whichever order we take for
applying rewriting rules, we finally reach from or T. $Applyarrow\cross orarrow+as$ far
as possible in the reductions from and . Then we get reductions $S4_{R}\infty Z$ andZ.

Proof:

$S$

$Z$

$T$

$Z$

$S$

$\tau\Rightarrow_{R}\infty$

$S$

$T$

1

Lemma 2.26
The same statement as the above lemma holds for some

Proof: Since$R_{i}$

instead of$R^{\infty}$.

is finite, only a finite number of Boolean variables appear in thealgorithm. Therefore, there are only a finite number of Boolean normal polynomials,
is finite. Therefore, there exists somesuch thatby definition
henceof. Clearly the assertion holds for this .
$E_{0}$$R^{\infty}$$R^{\infty}\subseteq R_{i}$$R_{i}$$R^{\infty}$$R_{i}$$1$

Proof of the last statement of the definition of the algorithm:
Take such that the above lemma holds. Since any $X$ inis reduced to;by applying Rules 1 and 2 several times, say k-times,
will be empty. Note that. To complete the proof, it suffices to show thethe above lemma also holds fornext lemma. 1$i$$E_{i}$$E_{i+k}$$R_{i+k}$–11–$0by\Rightarrow R$

Lemma 2.27
Let be an ideal generated by a finite set, $E$ , of Boolean normal polynomials. Thenfor each Boolean normal polynomial, $X$ and ,
$I$

$Y$

$X\equiv Y$$(mod I)$

iff.

$X^{*}rightarrow EY$

Proof:(if) It suffices to check the following. For each Boolean polynomial, $X$ and $Y$ , if$(mod I)$ . Let $X=BA+S,$ $Y=BW+S$ and$Xarrow zY$ for
in $E$ , then
$Z=A+W$ , then $(X+Y)\downarrow=(BA+S+BW+S)\downarrow=(B(A+W))\downarrow=(BZ)\downarrow\in I$ .
$Z$

$X\downarrow\equiv Y\downarrow$, $P_{n}\in E$ . Let $Z_{i}=$(only if) Suppose $X+Y=P_{1}X_{1}+P_{2}X_{2}+\ldots+P_{n}X_{n}$ for$Y+P_{1}X_{1}+P_{2}X_{2}+\ldots+P_{i}X_{i}$ for each $0\leq i\leq n$ . Then $Zarrowarrow*Z_{i-1}+P_{i}X_{1}=Z_{i}$ .
Combining these proofs obtains a proof of $X=Z_{0^{rightarrow E}}^{*}Z_{n}=Y.$$P_{1},$ $P_{2},$$\ldots$$[$

This completes the proof of Theorem 2.8.

REFERENCES[Bachmair 86] Bachmair, L., Dershowitz, N., and Hsiang, J.: Ordering for equational
proof, Proc. Symp. Logic in Computer Science, Cambridge, Massachusetts (June1986)[Buchberger 83] Buchberger, B.: Grobner Bases: An Algorithmic Method in Polynomial Ideal Theory, $T\varphi hnical$ Report, CAMP-LINTZ (Nov. 1983)[Dershowitz 79] Dershowitz, N. and Manna, Z.: Proving termination with multiset
orderings, Comm. ACM 22, pp. 465-467 (1979)[Dickson 13] Dickson, L. E.: Finiteness of the odd perfect and primitive abundant
numbers with n distinct prime factors, Am. J. of Math., vol. 35, pp. 413-426(1913)[Huet 80] Huet, G. and Oppen, D. C.: Equations and Rewrite Rules: a survey,
Formal Language: Perspectives and Open Problems Academic Press, pp. 349-405(1980)[Knuth 70] Knuth, D. E. and Bendix, P. B.: Simple word problems in universal
algebras, Computational problems in abstract algebra, Pergamon Press, Oxford(1970)[Waerden 37]

van der Waerden, B. L.: Moderne Algebra I, Berlin-Leipzig (1937)[Waerden 40]

van der Waerden, B. L.: Moderne Algebra II, Berlin-Leipzig (1940)–12–