Program schemata and the first-order decision problem

摘要

In [7] Manna reduces certain decision problems for program schemata to the problem of determining whether or not a first-order formula is satisfiable. Here we give an improved construction, which yields new positive results and suggests a method that may be useful in further investigations.