A Vernacular for Coherent Logic

TL;DR

This paper introduces a simple, expressive proof representation based on coherent logic, enabling easy generation of proofs across various proof assistants and formats, supported by tools and automated theorem proving capabilities.

Contribution

It presents a new proof representation using coherent logic, with accompanying XML format and transformations for multiple proof assistants and natural language formats.

Findings

Proofs can be generated for Isabelle/Isar and Coq

Automated theorem prover exports proofs in the new format

Tools and sample theorems are publicly available

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.