Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy - Artificial Intelligence and Symbolic Computation - page 246

of polynomial domains and study which ones will work. Interestingly, in the
literature, so far all methods for constructing Grobner bases rely on the critical-
pair-completion scheme in one way or the other and no drastically different
method has been found!)
The scheme for the unknown algorithm A involves the two unknown auxil-
iary functions lc and df . We now start an (automated) proof of the correctness
theorem for A , i.e. the theorem

is-finite-Grobner-basis [ A [ F ]]
generate-the-same-ideal [ F, A [ F ]]

.

∀ F

Of course, this proof will fail because nothing is yet known about the aux-
iliary functions lc and df . We now analyze carefully the situation in which the
proof fails and try to guess requirements lc and df should satisfy in order to be
able to continue with the correctness proof. It turns out that a relatively simple
requirements generation techniques suces for generating, completely automat-
ically, the following requirement for lc

lp [ g 1] | lc [ g 1 ,g 2]

lp [ g 2] | lc [ g 1 ,g 2]

lp [ g 1]

p )

∀ g 1 ,g 2 ,

| p

∀ p

p ⇒

( lc [ g 1 ,g 2] |

lp [ g 2] |

where lp [ f ] denotes the leading power product of polynomial f .Thisisnow
again an explicit problem specification, this time for the unknown function lc .
We could again run another round of our algorithm synthesis procedure using
schemes and failing proof analysis for synthesizing lc . However, this time, the
problem is easy enough to see that the specification is (only) met by

lc [ g 1 ,g 2 ]= lcm [ lp [ g 1 ] ,lp [ g 2 ]] ,

where lcm [ p, q ] denotes the least common multiple of power products p and q .
In fact, the specification is nothing else then an implicit definition of lcm and we
can expect that an algorithm satisfying this specification is part of the knowledge
base K .
Heureka! We managed to get the main idea for the construction of Grobner
bases completely automatically by applying algorithm schemes, automated theo-
rem proving, and automated failing proof analysis. Similarly, in a second attempt
to complete the proof of the correctness theorem, one is able to derive that, as
a possible df , we can take just polynomial difference.
The current requirements generation algorithms from failing proof, roughly,
has one rule. Given the failing proof situation, collect all temporary assumptions
T [ x 0 ,...,A [ ... ] , ... ] and temporary goals G [ x 0 ,...m [ ...,A [ ... ] ,... ]], where m
is (one of) the auxiliary operations in the algorithm scheme for the unknown
algorithm A and x 0 , etc. are the current “arbitrary but fixed” constants, and
produce the following requirement for m :

∀ x,...,y,... ( T [ x,...,y,... ] ⇒ G [ x,...,m [ ...,y,... ]]) .