First-order logic reducible programs

Programs for which the least fixed point exists are considered. A program is first-order logic reducible (FOL-reducible) with respect to a set of integrity constraints if all its valid fixed points are least fixed points. For an FOL-reducible program, a logical assertion about least fixed points is reduced to a logical assertion about all first-order logic models. This makes it possible to characterize, in the first-order logic, some important `all states´ properties of programs for which no proof procedures exist in general. This method is applied to the following properties: containment of programs, independence of updates with respect to queries and integrity constraints, and characterization and implication of integrity constraints in programs. It is shown that the transitive closure of a graph if FOL-reducible with respect to the constraint of acyclicity. The `all states´ framework requires a modification of the standard treatment of fixed points and completed programs