The Coq mailing list

[Rajeev.Gore AT anu.edu.au]

Yes, the modal logic S5 is strange because there is no known
traditional sequent calculus for it which is cut-free. There are many
variations on the traditional sequent calculus which will give
cut-free systems, but they all involve some sort of extra machinery on
top of Gentzen's good old LK. I can provide pointers if you are
interested, but most of them are of proof theoretical interest only,
and are not amenable to automation.

The Logics Work Bench at the University of Bern
 http://www.lwb.unibe.ch/modules/s5/index.html
has a module for theorem proving in (propositional) S5. 
You can use it via the web too.

I cannot now remember the exact details of how the LWB people
implemented S5 but there are several well-known tricks:

a) For every formula A, there exists a formula B of modal depth at
 most 1 which is logically equivalent in S5 to A. That is, given A and
 having found B, the formula A <-> B is a theorem of S5. I think there
 is an algorithm for computing B from A in [1], and also possibly in
 [2].

b) Formula A is a theorem S5 iff formula <>[]A is a theorem of S4; see
   pages 223-225 of [2]. So you could use the well-known cut-free
   sequent calculus for S4, and this embedding.

The logic KT5 is indeed equivalent to S5 (= KT45 = KT4B) since
transitivity (4) can be derived from reflexivity (T) and euclideaness
(5). Unfortunately, I am not familiar with Sato's system so I cannot
offer any insight here.

Can someone please give me more information about Sato's work?

For more information about such tricks and details of sequent
(actually tableaux) calculi for basic modal logics see [3].
For more details on the TWB see
 http://www.lwb.unibe.ch/about/publications.html
and particularly, Alain Heuerding's phd dissertation (but it does not
seem to be available electronically).

[1]
@book{wallen-book,
AUTHOR = "L A Wallen",
TITLE = "Automated Deduction in Nonclassical Logics: Efficient 
Matrix Proof Methods for Modal and Intuitionistic Logics",
PUBLISHER = "MIT Press ",
YEAR = 1989
}

[2] @book{fitting-proof,
AUTHOR = "M. Fitting",
TITLE = "Proof Methods for Modal and Intuitionistic Logics",
VOLUME = "169",
SERIES = "Synthese Library",
PUBLISHER = "D. Reidel, Dordrecht, Holland",
YEAR = "1983"
}

[3]
@InCollection{gore-tableau-methods,
  author = {R Gor\'{e}},
  title = {Chapter~6: Tableau Methods for Modal and Temporal
                  Logics},
  booktitle = {Handbook of Tableau Methods},
  publisher = {Kluwer Academic Publishers},
  year = 1999,
  pages = {297-396},
  editor = {{M {D'Agostino}, D Gabbay, R H\"{a}hnle, J Posegga}},
  note = {\url{http://arp.anu.edu.au/~rpg}}
}
Old draft available from http://arp.anu.edu.au/~rpg  :)

Feel free to email me if anything is unclear.

Best wishes,
Raj

-- 
Rajeev Gore'             http://arp.anu.edu.au/~rpg
Automated Reasoning Group, 
Computer Sciences Laboratory,
Research School of Information Sciences and Engineering,
Australian National University, Canberra, ACT 0200, Australia
Tel: +61-2-61 25 86 03 Fax:+61-2-61 25 86 51  Email: 
Rajeev.Gore AT anu.edu.au
ANU CRICOS Provider Number - 00120C