Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue
 
home
browse
current
etoc
authors
subinfo
subscribers
samples

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 6, December 2002: pp. 993-1016

Display Calculi for Nominal Tense Logics

Stéphane Demri1 and Rajeev Goré2

1Lab. Spécification et Vérification, CNRS, UMR 8643, ENS de Cachan, 61, av. du Pdt Wilson, 94235 Cachan Cedex, France. E-mail: demri@lsv.ens-cachan.fr
2Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. E-mail: rpg@arp.anu.edu.au

We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L[ne]) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus [dgr]MNTL for MNTL mimic those of the display calculus [dgr]L[ne] for L[ne]. We show that every MNTL-valid formula admits a cut-free derivation in [dgr]MNTL. We also show that a restricted display calculus [dgr]MNTL, is not only complete for MNTL, but that it enjoys cut-elimination for arbitrary sequents. Finally, we give a weak Sahlqvist-type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon [dgr]MNTL and [dgr]MNTL respectively. The display calculi based upon [dgr]MNTL enjoy cut-elimination for valid formulae only, but those based upon [dgr]MNTL enjoy cut-elimination for arbitrary sequents.

Keywords: Nominal tense logics; display logic; cut elimination theorem; strong normalisation; Sahlqvist tense formulae

Table of Contents   Full-Text PDF (228 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement