<p>Certain cases of a conjecture of Erdos <a href="http://arxiv.org/abs/1402.2184" rel="nofollow">were converted to boolean formulas</a> </p>

<p>From the abstract</p>

<blockquote>
  <p>We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solver, one can obtain a discrepancy 2 sequence of length 1160 and a proof of the Erdos discrepancy conjecture for C = 2, claiming that no discrepancy 2 sequence of length 1161, or more, exists</p>
</blockquote>

<p>In the case when the formula is unsatisfiable "The size of the certificate is about 13 GB, and the time needed to verify the certificate was comparable with the time needed to generate it".</p>

<p>To my surprise the sizes of the relatively fast solved formulas
were <strong>much bigger</strong> than hard combinatorial problems like
factoring or inverting crypto hash function.</p>

<p>Formulas are at:  <a href="http://cgi.csc.liv.ac.uk/~konev/SAT14/" rel="nofollow">http://cgi.csc.liv.ac.uk/~konev/SAT14/</a></p>

<hr>

<p>Another example might be <a href="http://mathworld.wolfram.com/RobbinsConjecture.html" rel="nofollow">Robbins Conjecture</a> which was solved by <a href="http://www.cs.unm.edu/~mccune/papers/robbins/" rel="nofollow">computer</a>.</p>

CC BY-SA 3.0
2014-07-15T07:21:58.237Z
2014-07-16T12:10:54.677Z
2014-07-16T12:10:54.677Z
joro
<p>We have done this recently in several papers on the properties of automatic and related sequences.  For example, in the paper <a href="http://arxiv.org/pdf/1211.1301.pdf" rel="noreferrer">http://arxiv.org/pdf/1211.1301.pdf</a> we gave a description of the number of unbordered factors of length $n$ of the Thue-Morse sequence, answering some questions of Currie and Saari.  In the paper <a href="http://arxiv.org/pdf/1406.0670.pdf" rel="noreferrer">http://arxiv.org/pdf/1406.0670.pdf</a> we proved a conjecture on the avoidability of the pattern $x x x^R$ in binary sequences.  In both cases we express the assertion to be proved in a logical language, and then use a Presburger-arithmetic-type prover to prove the assertion.</p>

CC BY-SA 3.0
2014-07-14T17:20:07.043Z
2014-07-14T17:20:07.043Z
Jeffrey Shallit
<p>I think the most spectacular example of this approach is Thomas Hales' proof of the Kepler conjecture (aka Hilbert's 18th problem). </p>

<p>In the 1950s, Fejes Toth proved that the Kepler conjecture was equivalent to a large collection of formulas in the first-order theory of real closed fields. Since Tarski had shown this theory to be decidable, he went on to speculate that if a sufficiently fast computer could be built, the Kepler conjecture could be resolved by machine. </p>

<p>Half a century later, Thomas Hales actually made this strategy work (after proving a lot of difficult theorems to further simplify the set of formulas the computer needed to check)! </p>

CC BY-SA 3.0
2014-07-16T11:12:11.963Z
2014-07-16T11:12:11.963Z
Neel Krishnaswami
<p>I am curious to know when open problems have been solved by expressing them in a specific logic, and then showing that this logic is decidable. </p>

<p>I have two distinct cases in mind:</p>

<ul>
<li>The problem is about decidability of something, and it can be reformulated in a decidable logic.</li>
<li>The conjecture is just a yes/no property about some mathematical object, like twin-prime conjecture. Turn it into a decidable logical sentence, and run the algorithm to know the answer.</li>
</ul>

<p>In both cases, it would be interesting if the logic is created and shown decidable just to fit the problem.</p>

<lo.logic><reductions><decidability>
Solving problems by deciding a logic
Denis
# Solving problems by deciding a logic

(Asked by: username_0 on 2014-07-14)

I am curious to know when open problems have been solved by expressing them in a specific logic, and then showing that this logic is decidable.

I have two distinct cases in mind:

* The problem is about decidability of something, and it can be reformulated in a decidable logic.
* The conjecture is just a yes/no property about some mathematical object, like twin-prime conjecture. Turn it into a decidable logical sentence, and run the algorithm to know the answer.

In both cases, it would be interesting if the logic is created and shown decidable just to fit the problem.

**Tags:** lo.logic, reductions, decidability


---

## 3 answers

### Answer by username_3 on 2014-07-16. Score: 6 | Accepted answer

I think the most spectacular example of this approach is Thomas Hales' proof of the Kepler conjecture (aka Hilbert's 18th problem).

In the 1950s, Fejes Toth proved that the Kepler conjecture was equivalent to a large collection of formulas in the first-order theory of real closed fields. Since Tarski had shown this theory to be decidable, he went on to speculate that if a sufficiently fast computer could be built, the Kepler conjecture could be resolved by machine.

Half a century later, Thomas Hales actually made this strategy work (after proving a lot of difficult theorems to further simplify the set of formulas the computer needed to check)!


---

### Answer by username_1 on 2014-07-15. Score: 5

Certain cases of a conjecture of Erdos [were converted to boolean formulas](http://arxiv.org/abs/1402.2184)

From the abstract

> We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solver, one can obtain a discrepancy 2 sequence of length 1160 and a proof of the Erdos discrepancy conjecture for C = 2, claiming that no discrepancy 2 sequence of length 1161, or more, exists

In the case when the formula is unsatisfiable "The size of the certificate is about 13 GB, and the time needed to verify the certificate was comparable with the time needed to generate it".

To my surprise the sizes of the relatively fast solved formulas
were **much bigger** than hard combinatorial problems like
factoring or inverting crypto hash function.

Formulas are at: <http://cgi.csc.liv.ac.uk/~konev/SAT14/>

---

Another example might be [Robbins Conjecture](http://mathworld.wolfram.com/RobbinsConjecture.html) which was solved by [computer](http://www.cs.unm.edu/~mccune/papers/robbins/).


---

### Answer by username_2 on 2014-07-14. Score: 5

We have done this recently in several papers on the properties of automatic and related sequences. For example, in the paper <http://arxiv.org/pdf/1211.1301.pdf> we gave a description of the number of unbordered factors of length $n$ of the Thue-Morse sequence, answering some questions of Currie and Saari. In the paper <http://arxiv.org/pdf/1406.0670.pdf> we proved a conjecture on the avoidability of the pattern $x x x^R$ in binary sequences. In both cases we express the assertion to be proved in a logical language, and then use a Presburger-arithmetic-type prover to prove the assertion.


---

