We propose an approach for defining labeled natural deduction systems for the class of Peircean branching temporal logics, seen as logics in their own right rather than as sub logics of Ockhamist systems. In particular, we give a system for the logic UB, i.e., the until-free fragment of CTL, and show that it is sound and complete. We also study normalization and discuss how derivations may reduce to a normal form using an appropriate management of proof contexts. Finally, we briefly discuss how to extend our system in order to capture full CTL.

A labeled deduction system for the logic UB

VIGANO', Luca;VOLPE, Marco
2013

Abstract

We propose an approach for defining labeled natural deduction systems for the class of Peircean branching temporal logics, seen as logics in their own right rather than as sub logics of Ockhamist systems. In particular, we give a system for the logic UB, i.e., the until-free fragment of CTL, and show that it is sound and complete. We also study normalization and discuss how derivations may reduce to a normal form using an appropriate management of proof contexts. Finally, we briefly discuss how to extend our system in order to capture full CTL.
Formal methods; temporal logic; Temporal Reasoning
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/11562/747769
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact