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.
CITATION STYLE
Stojanović, S., Narboux, J., Bezem, M., & Janičić, P. (2014). A vernacular for coherent logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8543 LNAI, pp. 388–403). Springer Verlag. https://doi.org/10.1007/978-3-319-08434-3_28
Mendeley helps you to discover research relevant for your work.