How to get more out of your oracles
From MaRDI portal
Publication:1687729
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
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