Preface

Funding

We have considered second-order quantifier elimination for a class of relational formulas characterized by a restriction of the quantifier prefix: existential predicate quantifiers followed by universal individual quantifiers. The main original motivation was to transfer instance-based techniques from automated theorem proving to second-order quantifier elimination. The technical result, however, does not indicate an immediate possibility for such a transfer, but gives some insight into the elimination problem for this class: The set of elimination resultants of a given formula and the set of formulas entailing the given second-order formula of that class is co-recursively enumerable. Candidate resultants can be generated, and there is an algorithm that halts on exactly those candidates that are not a resultant. Similarly, there is a method to detect that a given first-order formula does not entail the given second-order formula. By comparing formulas with respect to their first-order consequences, it is possible to express the respective theorem statements in a generalized way that applies to given second-order formulas independently of whether they have a resultant. These results were proven on the basis of small number of formula-based tools used in automated deduction. Actually, the results and involved constructions might be seen as a specialization to a formula class of Craig’s setting of determining recursive bases for subtheories of first-order formulas. The hope is that some inspiration and material for further investigation of “eliminability”, that is, existence of a resultant, or, more generally, of a formula that is equivalent with respect to first-order consequences, is provided. Acknowledgments. This work was supported by DFG grant WE 5641/1-1.