Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] are there specialists in linear algebra in the room?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] are there specialists in linear algebra in the room?


Chronological Thread 
  • From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] are there specialists in linear algebra in the room?
  • Date: Mon, 26 Sep 2016 14:56:08 +0200

Very interesting indeed. Thanks for the explanation.

On Mon, Sep 26, 2016 at 12:04:13PM +0200, Laurent Thery wrote:
>
>
> On 09/26/2016 11:30 AM, Daniel de Rauglaudre wrote:
> >Question: I was even not able to prove it with pen and paper!
> >How did nsatz do it? Is it possible to see its proof, except
> >by typing "Show Proof"?
>
> nsatz just implements the test for ideal membership using grobner basis.
>
> Given polynomials P1.. Pn and Q, it checks if Q is in the ideal
> generated by P1 .. Pn, ie if Q can be written as Q = \sum_i Pi * Ri
> for some arbitrary polynomials Ri.
> This solves exactly your problem that is P1= 0 -> ... -> Pn= 0 -> Q = 0.
>
> The problem is decided by building a "canonical" base for the ideal
> (P1,..Pn) using a completion à la Knuth-Bendix.
> What you have when you do Show Proof is mainly the Ri. Of course
> this is a bit obfuscated by the reification process.
> Anyway this output is usually not for human consumption, nsatz does
> not try to get the "smallest" certificate....
>
> Hope this helps
>
> --
> Laurent

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/



Archive powered by MHonArc 2.6.18.

Top of Page