Summary: In J.-L. Lassez and K. Marriott [J. Autom. Reasoning 3, 301–317 (1987; Zbl 0641.68124)], explicit and implicit generalizations were studied as representations of subsets of some fixed Herbrand universe \(H.\) An explicit generalization \(E=r_{1}\lor \cdots \lor r_{l}\) represents all ground terms that are instances of at least one of the terms \(t_{i},\) whereas an implicit generalization \(I=t/t_{1}\lor \cdots \lor t_{m}\) represents all \(H\)-ground instances of \(t\) that are not instances of any term \(t_{i}.\) More generally, a disjunction \(I=I_{1}\lor \cdots \lor I_{n}\) of implicit generalizations contains all ground terms that are contained in at least one of the implicit generalizations \(I_{j}.\) Implicit generalizations have applications to many areas of Computer Science like machine learning, unification, specification of abstract data types, logic programming, functional programming, etc. In these areas, the so-called finite explicit representability problem plays an important role, i.e. given a disjunction of implicit generalizations \(I=I_{1}\lor \cdots \lor I_{n}\), does there exist an explicit generalization \(E,\) s.t. \(I\) and \(E\) are equivalent?
We prove the coNP-completeness of this decision problem. Implicit generalizations can be represented as equational formulae, i.e., first-order formulae whose only predicate symbol is syntactic equality. Closely related to the finite explicit representability problem is the so-called negation elimination problem of equational formulae, i.e. given an arbitrary equational formula \(P,\) is \(P\) semantically equivalent to an equational formula without universal quantifiers and negation. In this work we study the negation elimination problem of equational formulae with purely existential quantifier prefix. We prove the coNP-completeness for such formulae in DNF and the \(\Pi_{2}^{p}\)-hardness in case of CNF.