Proving formally the implementation of an efficient gcd algorithm for polynomials

Mahboubi, Assia ; Mathematical, Reasoning and Software (MARELLE) ; et al.

In: Automated Reasoning, Third International Joint Conference, IJCAR 2006 ; https://hal.inria.fr/inria-00001270 ; Automated Reasoning, 2006

Online Konferenz

Wie komme ich dran?

Zugriff:

Volltext

Last version published in the proceedings of IJCAR 06, part of FLOC 06. ; International audience ; We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correction of our implementation of the subresultant algorithm. Up to our knowledge, it is the first mechanized proof of this result.

Titel:	Proving formally the implementation of an efficient gcd algorithm for polynomials
Autor/in / Beteiligte Person:	Mahboubi, Assia ; Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Ulrich Furbach and Natarajan Shankar
Link:	https://hal.inria.fr/inria-00001270 https://hal.inria.fr/inria-00001270/document Volltext
Zeitschrift:	Automated Reasoning, Third International Joint Conference, IJCAR 2006 ; https://hal.inria.fr/inria-00001270 ; Automated Reasoning, 2006
Veröffentlichung:	HAL CCSD ; Springer, 2006
Medientyp:	Konferenz
Schlagwort:	Seattle WA United States Coq computer algebra subresultants polynomials gcd formal proofs [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Subject Geographic: Seattle WA United States
Sonstiges:	Nachgewiesen in: BASE Sprachen: English Collection: Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) Document Type: conference object Language: English Relation: inria-00001270; https://hal.inria.fr/inria-00001270; https://hal.inria.fr/inria-00001270/document; https://hal.inria.fr/inria-00001270/file/SousRes.pdf Rights: info:eu-repo/semantics/OpenAccess

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.