June 2001
Intermediate to advanced
2128 pages
82h 43m
English
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.
Read now
Unlock full access