Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] On the uses of the algebra method.

Email Gateway (Aug 22 2022 at 21:11):

From: Javier Castellano <javier.castellano.manzano@gmail.com>
I have been using for a while the algebra method in Isabelle and I was
wondering if I could get some precisions on its behaviour. The relevant
manual section is "Algebraic reasoning via Gröbner bases". It indicates
that the method handles to main classes of problems:

1. Universal problems over multivariate polynomials in a (semi)-
   ring/field/idom.

What is meant by a universal problem in this context?

2. All-exists problems of the following restricted (but useful) form (the
   document specifies the formula).

What is meant by all-exists problems? Is it that it finds all the possible
tuples (y_1,...,y_k) satisfying the formula?

Many thanks

Last updated: Nov 21 2024 at 12:39 UTC