A Vernacular for Coherent Logic

Sana Stojanovic 1 Julien Narboux 2 Marc Bezem 3 Predrag Janicic 1
2 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rules and is based on a frag- ment of first-order logic called coherent logic. Coherent logic has been recognized by a number of researchers as a suitable logic for many ev- eryday mathematical developments. The proposed proof representation is accompanied by a corresponding XML format and by a suite of XSL transformations for generating formal proofs for Isabelle/Isar and Coq, as well as proofs expressed in a natural language form (formatted in LATEX or in HTML). Also, our automated theorem prover for coherent logic exports proofs in the proposed XML format. All tools are publicly available, along with a set of sample theorems.
Type de document :
Communication dans un congrès
CICM 2014 - Conferences on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. Springer, 8543, pp.16, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08434-3_28〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00983975
Contributeur : Julien Narboux <>
Soumis le : mercredi 14 mai 2014 - 09:33:03
Dernière modification le : lundi 6 mars 2017 - 13:39:42
Document(s) archivé(s) le : jeudi 14 août 2014 - 11:06:04

Fichiers

CLvernacular.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Sana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic. A Vernacular for Coherent Logic. CICM 2014 - Conferences on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. Springer, 8543, pp.16, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08434-3_28〉. 〈hal-00983975v2〉

Partager

Métriques

Consultations de la notice

165

Téléchargements de fichiers

243