A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions
Logic in Computer Science
2023-10-09 v1
Abstract
We present an incomplete proof synthesis method for the Calculus of Constructions which is always terminating and a complete Vernacular for the Calculus of Constructions based on this method.
Cite
@article{arxiv.2310.04090,
title = {A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2310.04090},
year = {2023}
}