A complete axiom system for propositional projection temporal logic with cylinder computation model

DOI10.1016/j.tcs.2015.05.007zbMath1332.68145OpenAlexW346741227WikidataQ114013034 ScholiaQ114013034MaRDI QIDQ896162

Nan Zhang, Cong Tian, Zhenhua Duan

Publication date: 11 December 2015

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

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

zbMATH Keywords

verificationaxiom systemmodel checkingspecificationpropositional projection temporal logiccylinder computation modelmulti-core parallel programs

Mathematics Subject Classification ID

Related Items (3)

Temporal logic specification mining of programs ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Index set expressions can represent temporal logic formulas

Uses Software

• ACL2
• Isabelle
• ML
• SPIN
• HOL
• CESAR

Cites Work

• A cylinder computation model for many-core parallel computing
• A complete proof system for propositional projection temporal logic
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A practical decision procedure for propositional projection temporal logic with infinite models
• Isabelle. A generic theorem prover
• Expressiveness of propositional projection temporal logic with star
• A decision procedure for propositional projection temporal logic with infinite models
• Temporal logic can be more expressive
• Automated Theorem Proving: After 25 Years
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A complete axiom system for propositional projection temporal logic with cylinder computation model