Synthesis of positive logic programs for checking a class of definitions with infinite quantification

We describe a method based on unfold/fold transformations that synthesizes positive logic programs P(r)P(r) with the purpose of checking mechanically definitions of the form D(r)=∀X(r(X)⇔QYR(X,Y))D(r)=∀X(r(X)⇔QYR(X,Y)) where r   is the relation defined by the formula QYR(X,Y)QYR(X,Y), X is a set of variables to be instantiated at runtime by ground terms, QY is a set of quantified variables on infinite domains (Q   is the quantifier) and R(X,Y)R(X,Y) a quantifier-free formula in the language of a first-order logic theory. This work constitutes a first step towards the construction of a new type of assertion checkers with the ability of handling restricted forms of infinite quantification.