How to get more out of your oracles
From MaRDI portal
Recommendations
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
- Formally proving size optimality of sorting networks
- Formalizing size-optimal sorting networks: extracting a certified proof checker
- Formal and efficient primality proofs by use of computer algebra oracles
- Oracle-based checking of untrusted software
Cites work
- A SAT attack on the Erdős discrepancy conjecture
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Formally proving size optimality of sorting networks
- Formally proving the Boolean Pythagorean triples conjecture
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- Mechanical verification of SAT refutations with extended resolution
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Sorting nine inputs requires twenty-five comparisons
- Theorem Proving in Higher Order Logics
This page was built for publication: How to get more out of your oracles
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687729)