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