Information Technology Reference

In-Depth Information

(defun-sk<k> in<> (p F)

(exists (C) (and (k-polynomialsp C) (equal p (lin-comb C F)))))

The use of
exists
in this definition is just syntactic sugar. Roughly speaking,

the above construction introduces a Skolem function
in<>-witness
,withargu-

ments
p
and
F
, which is axiomatized to choose, if possible, a list
C
of polynomial

coecients such that when linearly combined with the polynomials in
F
,
p
is ob-

tained. Thus,
C
is a witness of the membership of
p
to the ideal generated by
F
,

and
in<>
is defined by means of
in<>-witness
. The following theorems establish

that our definition of ideal in Acl2 meets the intended closure properties:

(defthm |p in <F> & q in <F> => p + q in <F>|

(implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F))

(implies (and (in<> p F) (in<> q F)) (in<> (+ p q) F))))

(defthm |q in <F> => p * q in <F>|

(implies (and (k-polynomialp p) (k-polynomialp q) (k-polynomialsp F))

(implies (in<> q F) (in<> (* p q) F))))

Whenever a theorem about
in<>
is proved we have to provide Acl2 with

a hint to construct the necessary witness. For example, to prove that polyno-

mial ideals are closed under addition we straightforwardly built an intermediate

function computing the witness of
p
+
q ∈F

from those of
p ∈F

and
q ∈F

.

Definition 3.
The congruence induced by an ideal

I
, written as

≡
I
, is defined

by
p ≡
I
q ⇐⇒ p − q ∈ I
.

The definition of

≡
F
in Acl2 is immediate
3
:

(defun<k> =<> (p q F)

(in<> (+ p (- q)) F))

Clearly, the ideal membership problem for an ideal
I

is solvable if, and only

if, its induced congruence

≡
I
is decidable. Polynomial reductions will help us to

design decision procedures for that congruence.

4

Polynomial Reductions

Let
<
M

= 0 a polynomial and let

lm
(
p
) denote the leader monomial of
p
with respect to
<
M
.

Definition 4.
Let
f

be a well-founded ordering on monomials,
p

=0
be a polynomial. The reduction relation on polynomi-

als induced by

f
, denoted as

→
f
,isdefinedsuchthat
p →
f
q

if

p
contains a

monomial
m

=0
such that there exists a monomial
c
such that
m
=

−c ·

lm
(
f
)

and

q

=

p
+
c · f
.If
F

=

{f
1
,...,f
k
}

is a finite set of polynomials, then the

→
F
=
i
=1
→
f
i
.

3
For the sake of readability, we use
defun-sk<k>
and
defun<k>
, instead of
defun-sk

and
defun
. These are just macros which add an extra parameter
k
(the number of

variables) to a function definition, so we do not have to specify it in each function

application. When
k
is not involved,
defun
is used.

reduction relation induced by
F

is defined as

Search WWH ::

Custom Search