Second-Order Characterizations of Definientia in Formula Classes

ABSTRACT. For a given formula, a definiens in terms of a given set of predicates can be characterized quite straightforwardly with predicate quantification. Methods for second-order quantifier elimination and the closely related computation of forgetting, projection and uniform interpolants can then be applied to compute such definientia. Here we address the question, whether also definientia that are in given classes of formulas, such as Horn formulas, conjunctions of atoms or Krom formulas, can be specified with predicate quantification and can thus be computed by second-order quantifier elimination methods.