Formally verifying the solution to the Boolean Pythagorean triples problem

DOI10.1007/S10817-018-9490-4MaRDI QIDQ2323449zbMATH OpenOpenAlexWikidataFDO

Authors Luís Cruz-Filipe, Peter Schneider-Kamp, Joao 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

interactive theorem provinglarge-scale proofsSAT solving

Mathematics Subject Classification ID

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

Recommendations

• Formally proving the Boolean Pythagorean triples conjecture
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Efficient verified (UN)SAT certificate checking
• Efficient, verified checking of propositional proofs
• Formal proof - the four color theorem

Cites work

• A machine program for theorem-proving
• Automated deduction -- CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6--11, 2017. Proceedings
• Blocked clause elimination
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Computer-aided proof of Erdős discrepancy properties
• Efficient certified RAT verification
• Efficient verified (UN)SAT certificate checking
• Extraction in Coq: An Overview
• Formally proving size optimality of sorting networks
• Formally proving the Boolean Pythagorean triples conjecture
• scientific article; zbMATH DE number 2033289 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8--12, 2017. Selected papers
• Mechanical verification of SAT refutations with extended resolution
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• The calculus of constructions
• The complexity of theorem-proving procedures
• Theorem Proving in Higher Order Logics
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing

Cited in

(9)

• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Formally proving the Boolean Pythagorean triples conjecture
• On multiple primitive Pythagorean triplets
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
• Certified logic-based explainable AI -- the case of monotonic classifiers
• Formal verification of the empty hexagon number
• A formal proof of R(4,5)=25
• A nonexistence certificate for projective planes of order ten with weight 15 codewords

Describes a project that uses

Uses Software

• Coq
• CoLoR
• CertiCoq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2323449)