A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions
arXiv:2310.04090
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.