The Explicit Representability of Implicit Generalizations

Abstract

In [9], implicit generalizations over some Herbrand universe H were introduced as constructs of the form I = t/t ₁ ∨. . . ∨t _m with the intended meaning that I represents all H-ground instances of t that are not instances of any term t _i on the right-hand side. More generally, we can also consider disjunctions $\mathcal{I} = I_{1} \vee . . . \vee I_n$ of implicit generalizations, where $\mathcal{I}$ contains all ground terms from H that are contained in at least one of the implicit generalizations I _j . Implicit generalizations have applications to many areas of Computer Science. For the actual work, the so-called finite explicit representability problem plays an important role, i.e.: Given a disjunction of implicit generalizations $\mathcal{I} = I_{1} \vee . . . \vee I_n$, do there exist terms r ₁,..., r _l , s.t. the ground terms represented by $\mathcal{I}$ coincide with the union of the H-ground instances of the terms r _j ? In this paper, we prove the coNP-completeness of this decision problem.