A polynomial translation of S4 into T and contraction-free tableaux for S4

The concern of this paper is the study of automated deduction methods for propositional modal logics. We use tableau proof-systems to show that Fitting's translation of the transitive modal logic S4 into T can be constructed in deterministic polynomial time. This result is exploited in order to establish a polynomial bound to the length of branches in both tableau and sequent proof search for the transitive logics S4 and K4. This allows the elimination of “periodicity tests” when proving S4-validity; moreover, it provides directly a form of “contraction elimination result” in modal sequent calculi, in the sense that the number of contractions needed in a branch of a sequent proof need not exceed a given polynomial function of the endsequent. In order to obtain a complete contraction free fragment of the sequent calculus for S4, Mints' translation of modal formulae into modal clauses is used. Mints' notion of modal clause is also used to provide polynomial translations of S4 and K4 into K, by means of a preliminary (polynomial) rewriting of the input formulae into clausal form.