Formally verifying the solution to the Boolean Pythagorean triples problem

DOI10.1007/s10817-018-9490-4zbMath1468.68318OpenAlexW2898484043WikidataQ114226107 ScholiaQ114226107MaRDI QIDQ2323449

Luís Cruz-Filipe, Peter Schneider-Kamp, João P. Marques-Silva

Publication date: 2 September 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9490-4

zbMATH Keywords

SAT solvinginteractive theorem provinglarge-scale proofs

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Ramsey theory (05D10) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Related Items (4)

Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification ⋮ Unnamed Item ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ A nonexistence certificate for projective planes of order ten with weight 15 codewords

Uses Software

• Coq
• CoLoR
• CertiCoq

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Computer-aided proof of Erdős discrepancy properties
• The calculus of constructions
• Formally proving size optimality of sorting networks
• Automated deduction -- CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6--11, 2017. Proceedings
• Efficient certified RAT verification
• 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
• Extraction in Coq: An Overview
• Blocked Clause Elimination
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing
• Formally Proving the Boolean Pythagorean Triples Conjecture
• Mechanical Verification of SAT Refutations with Extended Resolution
• Theorem Proving in Higher Order Logics
• A machine program for theorem-proving
• The complexity of theorem-proving procedures
• Efficient verified (UN)SAT certificate checking

This page was built for publication: Formally verifying the solution to the Boolean Pythagorean triples problem