A labelled sequent calculus is proposed for Priorean linear time logic, the rules of which reflect a natural closure algorithm derived from the fixed-point properties of the temporal operators. All the rules of the system are finitary, but proofs may contain infinite branches. Soundness and completeness of the calculus are stated with respect to a notion of provability based on a condition on derivation trees: A sequent is provable if and only if no branch leads to a ‘fulfilling sequent,’ the syntactical counterpart of a countermodel for an invalid sequent. Decidability is proved through a terminating proof search procedure, with an exponential bound to the branches of derivation trees for valid sequents, calculated on the length of the characteristic temporal formula of the endsequent.

Decidability for Priorean Linear Time Using a Fixed-Point Labelled Calculus / B. Boretti, S. Negri - In: Automated reasoning with automated tableaux and related methods : 18th international conference, Tableaux 2009, Oslo, Norway, July 6-10, 2009. proceedings / [a cura di] M. Giese, A. Waaler. - New York : Springer, 2009. - ISBN 9783642027154. - pp. 108-112 (( Intervento presentato al 18. convegno International Conference on Automated Reasoning with Analytic Tableaux and Related Methods tenutosi a Oslo nel 2009 [10.1007/978-3-642-02716-1_9].

Decidability for Priorean Linear Time Using a Fixed-Point Labelled Calculus

B. Boretti
Primo
;
2009

Abstract

A labelled sequent calculus is proposed for Priorean linear time logic, the rules of which reflect a natural closure algorithm derived from the fixed-point properties of the temporal operators. All the rules of the system are finitary, but proofs may contain infinite branches. Soundness and completeness of the calculus are stated with respect to a notion of provability based on a condition on derivation trees: A sequent is provable if and only if no branch leads to a ‘fulfilling sequent,’ the syntactical counterpart of a countermodel for an invalid sequent. Decidability is proved through a terminating proof search procedure, with an exponential bound to the branches of derivation trees for valid sequents, calculated on the length of the characteristic temporal formula of the endsequent.
Proof Analysis ; Temporal Logic ; Labelled Sequent Calculi
Settore M-FIL/02 - Logica e Filosofia della Scienza
2009
University of Oslo
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/2434/214254
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 5
social impact