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.
•