Prove:

(Formula (Test): B1) ,

with no assumptions.

Proved.

The Theorem is proved by the Groebner Bases method.      

      The formula in the scope of the universal quantifier is transformed into an equivalent formula that is a conjunction of disjunctions of equalities and negated equalities. The universal quantifier can then be distributed over the individual parts of the conjunction. By this, we obtain:

Independent proof problems:

(Formula (Test): B1.1)

(Formula (Test): B1.2)

We now prove the above individual problems separately:

Proof of ():

This proof problem has the following structure:

(Formula (Test): B1.1.structure) ,

where

() is equivalent to

(Formula (Test): B1.1.implication) .

() is equivalent to

(Formula (Test): B1.1.not-exists) .

By introducing the slack variable(s)

{ξ}

() is transformed into the equivalent formula

(Formula (Test): B1.1.not-exists-slack) .

Hence, we see that the proof problem is transformed into the question on whether or not a system of polynomial equations has a solution or not. This question can be answered by checking whether or not the (reduced) Groebner basis of

is exactly {1}.                  

Hence, we compute the Groebner basis for the following polynomial list:

The Groebner basis:

Hence, () is proved.

Proof of ():

This proof problem has the following structure:

(Formula (Test): B1.2.structure) ,

where

() is equivalent to

(Formula (Test): B1.2.implication) .

() is equivalent to

(Formula (Test): B1.2.not-exists) .

By introducing the slack variable(s)

{ξ1, ξ2}

() is transformed into the equivalent formula

(Formula (Test): B1.2.not-exists-slack) .

Hence, we see that the proof problem is transformed into the question on whether or not a system of polynomial equations has a solution or not. This question can be answered by checking whether or not the (reduced) Groebner basis of

is exactly {1}.                  

Hence, we compute the Groebner basis for the following polynomial list:

The Groebner basis:

Hence, () is proved.

Since all of the individual subtheorems are proved, the original formula is proved.

•

Additional Proof Generation Information

---

Converted by Mathematica      June 17, 2002