In this paper we provide tableau calculi for the intuitionistic modal logics LAX and LAX1, where the calculus for LAX1 is duplication-free while among the rules for LAX there is just one rule that allows duplication of formulas. These logics have been investigated by Fairtlough and Mendler in relation to the problem of Formal Hardware Verification. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Namely, we enlarge the language containing the usual sings T and F with the new sign Fc. LAX and LAX1 logics are characterized by a Kripke-semantics which is a ``weak" version of the semantics for ordinary intuitionistic modal logics. In this paper we establish the soundness and completeness theorems for these calculi.

Almost Duplication-Free Tableau Calculi for Propositional Lax Logics

FERRARI, MAURO
1996-01-01

Abstract

In this paper we provide tableau calculi for the intuitionistic modal logics LAX and LAX1, where the calculus for LAX1 is duplication-free while among the rules for LAX there is just one rule that allows duplication of formulas. These logics have been investigated by Fairtlough and Mendler in relation to the problem of Formal Hardware Verification. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Namely, we enlarge the language containing the usual sings T and F with the new sign Fc. LAX and LAX1 logics are characterized by a Kripke-semantics which is a ``weak" version of the semantics for ordinary intuitionistic modal logics. In this paper we establish the soundness and completeness theorems for these calculi.
1996
Pierangelo Miglioli and Ugo Moscato and Daniele Mundici and Mario Ornaghi
Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15-17, 1996, Proceedings
3540612084
Theorem Proving with Analytic Tableaux and Related Methods
Terrasini, Palermo, ITALY
May 15-17, 1996
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: https://hdl.handle.net/11383/1756904
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 1
social impact