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.
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
p contains a
monomial m
=0 such that there exists a monomial c such that m =
−c ·
lm ( f )
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