Establishing Complexity Bounds

Three aspects are of importance when using Saturate to derive complexity bounds for entailment.

• We need to use an ordering in which ground terms have at most finitely many smaller terms. An lpo is, hence, in most cases not suitable.
• The treatment of transitive relations by chaining has to be turned off (cf. flag settings) to invoke ordered resolution also for transitive relations and, in particular, for the transitivity axiom itself.
• No selection of negative literals is allowed, cf. command sass.

For establishing a polynomial complexity bound, the (precedence-modified) subterm ordering sto should be chosen with an appropriate ordering declaration. Finitely saturating a theory under an instance of this class of partial orderings (actually one saturates with respect to all possible well-founded completions of that instance simultaneously) proves that the entailment problem for the respective theory is decidable in polynomial time if the theory is Horn, and in CoNP, if it is not Horn. We refer to (Basin & Ganzinger, 1995) for a detailed explanation of the theoretical basis.

The subdirectory LocalTheories of saturate/examples shows examples that we have saturated with respect to the sto, including the theory of term embedding, congruence closure, various fragments of propositional calculus, and the largest PTIME fragment of Allen's interval logic: the theory of partial nonstrict orderings. A formulation of sequent calculus has been saturated modulo AC and with respect to a linear interpretation function as ordering. The details are explained in the respective file. Term orderings via linear interpretations are available only in the Saturate version under SICStus 3.0. Such interpretations may be useful when one intends to prove exponential upper bounds for the complexity of entailment problems.

Proving the locality of a theory usually requires clausal rewriting with an appropriate setting of sarp. in addition to the usual simplification and deletion techniques. In some cases hereditary ordering constraints with sass([2]) will be useful.

Imprint | Data Protection