Boolean unification with predicates
Sebastian Eberhard, Stefan Hetzl, Daniel Weller · Journal of Logic and Computation · 2015
In this article, we deal with the following problem which we call Boolean unification with predicates: For a given formula F[X] in first-order logic with equality containing an n-ary predicate variable X, is there a quantifier-free formula G[x1,…,xn] such that the formula F[G] is valid in first-order logic with equality? We obtain the following results. Boolean unification with predicates for quantifier-free F is Π2P-complete. In addition, there exists an EXPTIME algorithm which for an input formula F[X], given as above, constructs a formula G such that F[G] being valid in first-order logic with equality, if such a formula exists. For F of the form ∀y¯F′[X,y¯] with F′ quantifier-free, we prove that Boolean unification with predicates is already undecidable. The same holds for F of the form ∃y¯F′[X,y¯] for F′ quantifier-free. Instances of Boolean unification with predicates naturally occur in the context of automated theorem proving. Our results are relevant for cut-introduction and the automated search for induction invariants.