I was reading this paper http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.117.2911&rep=rep1&type=pdf in which the author describes an algorithm, based on Groebner basis, whose input is a proposition in Peano arithmetic that satisfies a specific quantifier structure, and the output is True or False. If the output is true, then the proposition must be true. However, sometimes the output is false but the proposition is true, so the algorithm is not a decision procedure for Peano arithmetic -I already know that such an algorithm cannot exist, by Matiyasevich theorem-.
I have two questions:
1: Are there any similar results to this, i.e. an efficient pseudo-decision procedure such that if the output is true, then the proposition must be true, but we cannot say anything in the other case?
2: Is there a chance to use similar ideas to the ones in the paper so that we can overcome the limitations on the quantifier structure of the input propositions, and ask things like "There are many infinitely many prime numbers"?