Handbook of Automated Reasoning

6.1 Saturating background theories

The fact that no positive R-literals occur in semi-functional translation of modal formulae can be used by pre-computing everything that can possibly be derived from the background theory, i.e., this theory gets saturated. Such a saturation characterizes the modal logic and is thus independent of the theorem to be proved.

6.4. Definition

We call a clause C p-positive (p-negative) if there is a positive (negative) occurrence of a p-literal in C. If, in addition, C is not p-negative (not p-positive) then we call C pump-positive (pure-p-negative).

6.5. Definition

((Partial) Saturation). Let p be a designated predicate symbol and let $\mathcal{C}$ be a set of p-positive clauses. The saturation of C with respect ...