Saturation of a Theory

When we are interested in the finite saturation of a theory, we don't expect to find a contradiction and hence want to limit forward computation as much as possible. In that case we might want to switch on some of the more complex proof techniques for redundancy such as case analysis or clausal rewriting (cf. sarp command). Case analysis is particularly useful in the presence of AC-symbols. Clausal rewriting has no effect on purely equational theories. It works best in a resolution context when equality plays no role at all. The positive selection strategy (sass([2])) is usually not appropriate in this context. Usually the lexicographic path orderings lpo and aclpo with an aprropriately defined precedence work best in this context. Once we have managed to saturate a theory finitely, all proofs with respect to that theory are linear in the sense that they have the set-of-support property.

Imprint | Data Protection