| Decidability of Modal System S5: A Recursive Algorithm. (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract.- The decidability method, given in [6], for modal system S5 uses the reduced modal normal form. In this paper we present a recursive algorithm for computing the reduced modal normal form and use this algorithm as a subroutine for an algorithm deciding validity of formulas of system S5. | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||