O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 C be a set of p-positive clauses. The saturation of C with respect ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required