Authors
Rajeev Prakhakar Goré
Publication date
1992
Issue
UCAM-CL-TR-257
Publisher
University of Cambridge, Computer Laboratory
Description
We present a unified treatment of tableau, sequent and axiomatic formulations for many propositional normal modal logics, thus unifying and extending the work of Hanson, Segerberg, Zeman, Mints, Fitting, Rautenberg and Shvarts. The primary emphasis is on tableau systems as the completeness proofs are easier in this setting. Each tableau system has a natural sequent analogue defining a finitary provability relation for each axiomatically formulated logic L. Consequently, any tableau proof can be converted into a sequent proof which can be read downwards to obtain an axiomatic proof. In particular, we present cut-free sequent systems for the logics S4. 3, S4. 3.1 and S4. 14. These three logics have important temporal interpretations and the sequent systems appear to be new.
Total citations
1993199419951996199719981999200020012002200320042005200620072008200920102011201220132014201520162017201820192020202120222023202413131531211118131221