A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions
Voices Powered by
Connected to paperThis paper is a preprint and has not been certified by peer review
A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions
Gilles Dowek
AbstractWe 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.