© 2002 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original Article |
Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics
1 Dipartimento di Scienze dell'Informazione, Universita' degli Studi di Milano, Italy.E-mail: fiorino{at}dsi.unimi.it
In this paper we present duplication-free tableau calculi for three propositional intermediate interpolable logics, namely the logic characterized by rooted Kripke models with depth two at most, the logic characterized by rooted Kripke models with two final elements at most and depth two at most and the logic characterized by rooted Kripke models with a final element at most (also known as Jankov Logic). Using such calculi we define a O(n)-SPACE decision procedure for the second logic and a O(n log n)-SPACE decision procedure for each of the other two logics.
Keywords: Tableau systems; intermediate logics; decision procedures
Received 21 June 2000.