Automatic Proof Checking and Proof Construction by Tactics
Gilles Dowek
TL;DR
This paper compares proof verification systems and proposes a unified approach combining proof checking and tactic-based proof construction to improve mathematical development validation.
Contribution
It introduces a novel integrated system that merges proof checking and tactic-based proof construction methods.
Findings
Comparison of proof checking and tactic-based systems
Proposal of a unified proof system
Potential improvements in proof verification efficiency
Abstract
In this note we compare two kinds of systems that verify the correctness of mathematical developments: roof checking and proof construction by tactics and we propose to merge them in a single system.
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
TopicsMathematics, Computing, and Information Processing · Logic, programming, and type systems · History and Theory of Mathematics