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

DOI10.1016/J.TCS.2015.05.007zbMATH Open1332.68145OpenAlexW346741227WikidataQ114013034 ScholiaQ114013034MaRDI QIDQ896162FDOQ896162

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

Recommendations

• A complete proof system for propositional projection temporal logic
• A decision procedure and complete axiomatization for projection temporal logic
• Complete axiomatization for projection temporal logic with finite time
• Axiomatic semantics of projection temporal logic programs
• A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
• The axiomatization of propositional linear time temporal logic
• A Complete Proof System for First-order Interval Temporal Logic with Projection
• A complete axiom system for propositional interval temporal logic with infinite time
• An efficient decision procedure for propositional projection temporal logic
• Propositional temporal logics: decidability and completeness

zbMATH Keywords

verificationmodel checkingspecificationaxiom systempropositional projection temporal logiccylinder computation modelmulti-core parallel programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

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

Cited In (3)

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

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q896162)