I am looking for an example of decidable problems the decision procedures of which are unknown. I believe someone mentioned one to me once, and I also have read somewhere, but my memory is corrupted. I suppose the decidability of these problems are proved non-constructively, so that they have this kind of counter-intuitive property.
I think that in graph theory, there are a number of problems in this trait. I am wondering if you are aware of any of these.