Mathematics and Proof Presentation in Pcoq - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2001

Mathematics and Proof Presentation in Pcoq

Yves Bertot
Loïc Pottier
Laurence Rideau
  • Fonction : Auteur
  • PersonId : 832430

Résumé

We present PCOQ , a user-interface for the Coq system which provides elaborate mathematical formulas lay-out.We first show how the organization of thegraphic- al user-interface around structured data makes it possible to obtain this. In particular, we insist on the three-level extension mechanisms that supports the customiation of the layout for specific applications. In the next section, we describe the data-structure that is used in the logical engine to record proofs-in-the-making and we show this data-structure can be used as a basis to produce text in a restricted subset of natural language. Here, the natural text is still obtained by a layout strategy over a structured piece of data, and we show that interactive manipulation over this piece of data is still possible, thus providing ameans of developing proof, while looking directly at text being produced. We conclude by describin- g all the new questions that this experiment raises with respect to proof explanation and its integration in proof development environments.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-4313.pdf (278.41 Ko) Télécharger le fichier

Dates et versions

inria-00072274 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00072274 , version 1

Citer

Ahmed Amerkad, Yves Bertot, Loïc Pottier, Laurence Rideau. Mathematics and Proof Presentation in Pcoq. RR-4313, INRIA. 2001. ⟨inria-00072274⟩
235 Consultations
216 Téléchargements

Partager

Gmail Facebook X LinkedIn More