Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker

DOI10.1007/978-3-319-22102-1_10zbMath1465.68304arXiv1502.05209OpenAlexW3099329863MaRDI QIDQ2945629

Peter Schneider-Kamp, Luís Cruz-Filipe

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1502.05209

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof ⋮ Formally proving size optimality of sorting networks ⋮ Sorting nine inputs requires twenty-five comparisons

Cites Work

• Sorting nine inputs requires twenty-five comparisons
• Every planar map is four colorable. I: Discharging
• Every planar map is four colorable. II: Reducibility
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• A SAT Attack on the Erdős Discrepancy Conjecture
• A computer-assisted optimal depth lower bound for nine-input sorting networks
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Toward a Lower Bound for Sorting Networks
• The challenge of computer mathematics
• Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
• Formalizing Bounded Increase
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker