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.