Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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?

  1. 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: Mar 29 2024 at 12:28 UTC