3527 articles – 5253 Notices  [english version]

hal-00580296, version 1

Label-free Natural Deduction Systems for Intuitionistic and Classical Modal Logics

Didier Galmiche () 1, Yakoub Salhi () 1

Journal of Applied Non Classical Logics 20, 4 (2010) 373-421

Résumé : In this paper we study natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple labelfree natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the subformula property in the intuitionistic case.

  • 1 :  TYPES (LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domaine : Informatique/Logique en informatique
 
  • hal-00580296, version 1
  • http://hal.archives-ouvertes.fr/hal-00580296
  • oai:hal.archives-ouvertes.fr:hal-00580296
  • Contributeur : Didier Galmiche <>
  • Soumis le : Dimanche 27 Mars 2011, 21:10:26
  • Dernière modification le : Mardi 29 Mars 2011, 14:10:12