Sequent calculi and decision procedures for weak modal systems

Studia Logica 66 (1):121-145 (2000)
  Copy   BIBTEX


We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of Löb rules are given.



    Upload a copy of this work     Papers currently archived: 89,764

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

45 (#307,672)

6 months
3 (#435,525)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Investigations into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.
Proof Methods for Modal and Intuitionistic Logics.Melvin Fitting - 1985 - Journal of Symbolic Logic 50 (3):855-856.
Modalité monotone et schéma T.Thierry Lucas - 1991 - Logique Et Analyse 133 (134):151-158.

Add more references