A decidable fragment of the elementary theory of relations and some applications
Domenico Cantone, Vincenzo Cutello · 1990
The class of purely universal formulae of the elementary theory of relations with equality is shown to have an NP-complete satisfiability problem, under the assumption that there is an a priori bound on the length of quantifier prefixes and the arities of relation variables. In the second part of the paper we discuss possible applications in the field of theorem proving in set and graph theory and of consistency checking for queries in relational databases.