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.

Cerrito S, & Cialdea Mayer M (1997). A polynomial translation of S4 into T and contraction-free tableaux for S4. LOGIC JOURNAL OF THE IGPL, 5(2), 287-300.

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

CIALDEA, Marta
1997

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11590/119373
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact