A New Space Bound for the Modal Logics K4, KD4 and S4

We propose so called clausal tableau systems for the common modal logics K4, KD4 and S4. Basing on these systems, we give more efficient decision procedures than those hitherto known for the considered logics. In particular space requirements for our logics are reduced from the previously established bound O(n2 . log n) to O(n. log n).

• Type: Conference
• Year: 1999
• Where: MFCS
• Authors: Linh Anh Nguyen
• Keywords: Clausal Tableau Systems, Common Modal Logics, Log N, MFCS 1999, Theoretical Computer Science