A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions
Gilles Dowek
TL;DR
This paper introduces a proof synthesis algorithm for the Calculus of Constructions, providing a complete Vernacular and ensuring termination, thereby advancing formal proof development in this logical framework.
Contribution
It presents the first incomplete proof synthesis method that always terminates and a complete Vernacular for the Calculus of Constructions based on this method.
Findings
The proof synthesis method guarantees termination.
The Vernacular is complete for the Calculus of Constructions.
The approach improves proof automation in formal systems.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHistory and Theory of Mathematics · Mathematics, Computing, and Information Processing · Logic, programming, and type systems