Improved Decision Procedures for the Modal Logics K, T, and S4

We propose so called contraction free sequent calculi for the three prominent modal logics K, T, and S4. Deduction search in these calculi is shown to provide more efficient decision procedures than those hitherto known. In particular space requirements for our logics are lowered from the previously established bounds of the form n2 , n3 and n4 to n log n, n log n, and n2 log n respectively.

• Type: Conference
• Year: 1995
• Where: CSL
• Authors: Jörg Hudelmaier
• Keywords: Automated Reasoning, CSL 1995, Free Sequent Calculi, Log N, Prominent Modal Logics