How to get more out of your oracles

DOI10.1007/978-3-319-66107-0_11zbMath1483.68481OpenAlexW2749755840MaRDI QIDQ1687729

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

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)

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Sorting nine inputs requires twenty-five comparisons
• Formally proving size optimality of sorting networks
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• A SAT Attack on the Erdős Discrepancy Conjecture
• Formally Proving the Boolean Pythagorean Triples Conjecture
• Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
• Mechanical Verification of SAT Refutations with Extended Resolution
• Theorem Proving in Higher Order Logics

This page was built for publication: How to get more out of your oracles