### Resumé

Originalsprog | Engelsk |
---|---|

Titel | Proceedings of LPAR-21 : 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning |

Redaktører | Thomas Eiter, David Sands |

Forlag | EasyChair Publications |

Publikationsdato | 2017 |

Sider | 509-522 |

DOI | |

Status | Udgivet - 2017 |

Begivenhed | 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Maun, Botswana Varighed: 7. maj 2017 → 12. maj 2017 Konferencens nummer: 21 |

### Konference

Konference | 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning |
---|---|

Nummer | 21 |

Land | Botswana |

By | Maun |

Periode | 07/05/2017 → 12/05/2017 |

Navn | EPiC Series in Computing |
---|---|

Vol/bind | 46 |

ISSN | 2398-7340 |

### Fingeraftryk

### Citer dette

*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

}

*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.

Publikation: Bidrag til bog/antologi/rapport/konference-proceeding › Konferencebidrag i proceedings › Forskning › peer 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 -