We introduce a natural deduction system for the until-free subsystem BCTL*_ of the branching time logic BCTL. Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics.
A natural deduction system for bundled branching time logic / Baratella, Stefano; A., Masini. - In: JOURNAL OF APPLIED NON-CLASSICAL LOGICS. - ISSN 1166-3081. - ELETTRONICO. - 23:3(2013), pp. 268-283. [10.1080/11663081.2013.830401]
A natural deduction system for bundled branching time logic.
Baratella, Stefano;
2013-01-01
Abstract
We introduce a natural deduction system for the until-free subsystem BCTL*_ of the branching time logic BCTL. Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics.| File | Dimensione | Formato | |
|---|---|---|---|
|
JANCL_published.pdf
Solo gestori archivio
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
269.63 kB
Formato
Adobe PDF
|
269.63 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
