Title: Decidability for Priorean Linear Time Using a Fixed-Point Labelled Calculus
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.
Publication Year: 2009
Publication Date: 2009-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 6
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot