Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/517
Title: | A vernacular for coherent logic | Authors: | Stojanović, Sana Narboux, Julien Bezem, Marc Janičić, Predrag |
Affiliations: | Informatics and Computer Science | Issue Date: | 1-Jan-2014 | Related Publication(s): | International Conference on Intelligent Computer Mathematics CICM 2014 | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 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 fragment of first-order logic called coherent logic. Coherent logic has been recognized by a number of researchers as a suitable logic for many everyday 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 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. © 2014 Springer International Publishing. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/517 | ISBN: | 9783319084336 | ISSN: | 03029743 | DOI: | 10.1007/978-3-319-08434-3_28 |
Appears in Collections: | Research outputs |
Show full item record
SCOPUSTM
Citations
8
checked on Dec 20, 2024
Page view(s)
7
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.