ProofCloud: A Proof Retrieval Engine for Verified Proofs in Higher Order Logic
Shuai Wang
TL;DR
ProofCloud is a proof retrieval engine designed for higher order logic that enables fast proof searching, proof reuse, and includes comprehensive proof-checking results and benchmarks for the OpenTheory repository.
Contribution
It introduces ProofCloud, the first complete proof-checking system with benchmarks for the OpenTheory repository, enhancing proof reuse and verification in higher order logic.
Findings
Provides fast proof searching for higher order logic proofs.
Includes the first complete proof-checking results for OpenTheory.
Offers benchmarks demonstrating proof verification performance.
Abstract
This paper introduces ProofCloud, a proof retrieval engine for verified proofs in higher order logic. It provides a fast proof searching service for mathematicians and computer scientists for the reuse of proofs and proof packages. In addition, it includes the first complete proof-checking results and benchmarks of the OpenTheory repository.
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
TopicsLogic, programming, and type systems