# Solving problems by deciding a logic

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.

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)!

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.

Certain cases of a conjecture of Erdos were converted to boolean formulas

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 which was solved by computer.