Index set expressions can represent temporal logic formulas

DOI10.1016/j.tcs.2018.11.030zbMath1498.03047OpenAlexW2905458020WikidataQ128733895 ScholiaQ128733895MaRDI QIDQ2317353

Cong Tian, Qian Ma, Nan Zhang, Zhenhua Duan, Hongwei David Du

Publication date: 9 August 2019

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2018.11.030

zbMATH Keywords

algorithmstheorem provingfixed-pointmodel theorysemanticstemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44)

Related Items

A sound and complete proof system for a unified temporal logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A complete proof system for propositional projection temporal logic
• A practical decision procedure for propositional projection temporal logic with infinite models
• A formal proof of the deadline driven scheduler in PPTL axiomatic system
• A canonical form based decision procedure and model checking approach for propositional projection temporal logic
• A complete axiom system for propositional projection temporal logic with cylinder computation model
• Expressiveness of propositional projection temporal logic with star
• Framed temporal logic programming
• A decision procedure for propositional projection temporal logic with infinite models
• A lattice-theoretical fixpoint theorem and its applications
• Some Fixed-Point Issues in PPTL
• Twenty Years of Theorem Proving for HOLs Past, Present and Future
• An axiomatic basis for computer programming