Formally Proving the Boolean Triples Conjecture

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

59 Downloads (Pure)

Resumé

In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.
OriginalsprogEngelsk
TitelProceedings of LPAR-21 : 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
RedaktørerThomas Eiter, David Sands
ForlagEasyChair Publications
Publikationsdato2017
Sider509-522
DOI
StatusUdgivet - 2017
Begivenhed21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Maun, Botswana
Varighed: 7. maj 201712. maj 2017
Konferencens nummer: 21

Konference

Konference21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Nummer21
LandBotswana
ByMaun
Periode07/05/201712/05/2017
NavnEPiC Series in Computing
Vol/bind46
ISSN2398-7340

Fingeraftryk

Pythagorean
Natural numbers
Coloring
Encoding
Logic
Simplification
Formalization

Citer dette

Cruz-Filipe, L., & Schneider-Kamp, P. (2017). Formally Proving the Boolean Triples Conjecture. I T. Eiter, & D. Sands (red.), Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (s. 509-522). EasyChair Publications. EPiC Series in Computing, Bind. 46 https://doi.org/10.29007/jvdj
Cruz-Filipe, Luis ; Schneider-Kamp, Peter. / Formally Proving the Boolean Triples Conjecture. Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. red. / Thomas Eiter ; David Sands. EasyChair Publications, 2017. s. 509-522 (EPiC Series in Computing, Bind 46).
@inproceedings{e51a8ddd9752469b8270a08eb90cc8dc,
title = "Formally Proving the Boolean Triples Conjecture",
abstract = "In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.",
author = "Luis Cruz-Filipe and Peter Schneider-Kamp",
year = "2017",
doi = "10.29007/jvdj",
language = "English",
pages = "509--522",
editor = "Thomas Eiter and David Sands",
booktitle = "Proceedings of LPAR-21",
publisher = "EasyChair Publications",

}

Cruz-Filipe, L & Schneider-Kamp, P 2017, Formally Proving the Boolean Triples Conjecture. i T Eiter & D Sands (red), Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair Publications, EPiC Series in Computing, bind 46, s. 509-522, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 07/05/2017. https://doi.org/10.29007/jvdj

Formally Proving the Boolean Triples Conjecture. / Cruz-Filipe, Luis; Schneider-Kamp, Peter.

Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. red. / Thomas Eiter; David Sands. EasyChair Publications, 2017. s. 509-522 (EPiC Series in Computing, Bind 46).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Formally Proving the Boolean Triples Conjecture

AU - Cruz-Filipe, Luis

AU - Schneider-Kamp, Peter

PY - 2017

Y1 - 2017

N2 - In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.

AB - In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.

U2 - 10.29007/jvdj

DO - 10.29007/jvdj

M3 - Article in proceedings

SP - 509

EP - 522

BT - Proceedings of LPAR-21

A2 - Eiter, Thomas

A2 - Sands, David

PB - EasyChair Publications

ER -

Cruz-Filipe L, Schneider-Kamp P. Formally Proving the Boolean Triples Conjecture. I Eiter T, Sands D, red., Proceedings of LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair Publications. 2017. s. 509-522. (EPiC Series in Computing, Bind 46). https://doi.org/10.29007/jvdj