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