Domain-independent formulas and databases (Q1092679)

A proof theoretic characterization of domain-independent formulas in deductive databases is given. On the basis of equivalence to domain- independent formulas, a new class of formulas called ``allowed'' is defined. This leads to the proposed new notion of ``allowed'' databases. It is proved that every allowed database that is definite or hierarchical is domain-independent and that every domain-independent database has an equivalent allowed database (in a certain sense).