Establishing Complexity Bounds

This is a new application of saturation up to redundancy by ordered resolution. For a finitely presented saturated theory, depending on the ordering that was used for saturation, we may obtain a complexity result for the entailment problem for that theory. We call a theory local if it can be saturated up to redundancy for an ordering with a specific complexity bound. The setting of directives for establishing locality is discussed below. Specific orderings must be used and the full power with respect to redundancy proofs has to be requested.

Imprint | Data Protection