How to get more out of your oracles

DOI10.1007/978-3-319-66107-0_11MaRDI QIDQ1687729zbMATH OpenOpenAlexFDO

Authors Luís Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp

Publication date 4 January 2018

Full work available at URL https://doi.org/10.1007/978-3-319-66107-0_11

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

Cited in

(1)

• A good oracle is hard to beat

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)