Field : une procédure de décision pour les nombres réels en Coq / Field: a decision process for the real numbers in Coq

DELAHAYE, David ; MAYERO, Micaela

In: JFLA 2001 : journées francophones des langages applicatifs (Pontcarlier, 29-30 janvier 2001 ) :33-47

Konferenz - print, 12 ref

Nous nous proposons d'automatiser les preuves d'égalités sur les nombres réels dans le système Coq en utilisant la théorie des corps commutatifs. L'idée de l'algorithme consiste à se débarrasser des inverses afin de pouvoir se brancher sur la procédure de décision déjà existante sur les anneaux abéliens (Ring). L'élimination des inverses se fait de manière complètement réflexive et la réflexion est réalisée au moyen d'un nouveau langage de tactiques intégré au système Coq (version V7). Nous pensons étendre cette tactique à tous les corps commutatifs bien qu'actuellement, seuls les nombres réels soient concernés.

Titel:	Field : une procédure de décision pour les nombres réels en Coq / Field: a decision process for the real numbers in Coq
Autor/in / Beteiligte Person:	DELAHAYE, David ; MAYERO, Micaela
Link:	View record from PASCAL Archive
Quelle:	JFLA 2001 : journées francophones des langages applicatifs (Pontcarlier, 29-30 janvier 2001 ) :33-47
Veröffentlichung:	Le Chesnay: INRIA, 2001
Medientyp:	Konferenz
Umfang:	print, 12 ref
Schlagwort:	Computer science Informatique Sciences exactes et technologie Exact sciences and technology Sciences et techniques communes Sciences and techniques of general use Mathematiques Mathematics Algèbre Algebra Théorie des nombres Number theory Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Informatique théorique Theoretical computing Algorithmique. Calculabilité. Arithmétique ordinateur Algorithmics. Computability. Computer arithmetics Anneau Ring Anillo Démonstration automatique Automatic proving Demostración automática Démonstration théorème Theorem proving Demostración teorema Preuve programme Program proof Prueba programa Théorie abélienne Abelian theory Teoría abeliana Théorie nombre Teoría números Vérification programme Program verification Verificación programa Coq Nombre réel Real number
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: French Original Material: INIST-CNRS Document Type: Conference Paper File Description: text Language: French Author Affiliations: INRIA Rocquencourt, Projet LogiCal, Domaine de Voluceau BP 105, 78153 Le Chesnay, France Rights: Copyright 2002 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems ; Mathematics

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.