A complete proof system for propositional projection temporal logic
From MaRDI portal
Publication:391223
DOI10.1016/j.tcs.2012.01.026zbMath1417.03146OpenAlexW2094571962MaRDI QIDQ391223
Maciej Koutny, Nan Zhang, Zhenhua Duan
Publication date: 10 January 2014
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2012.01.026
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (13)
A temporal programming model with atomic blocks based on projection temporal logic ⋮ Unified temporal logic ⋮ A complete axiom system for propositional projection temporal logic with cylinder computation model ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ A proof system for unified temporal logic ⋮ A sound and complete proof system for a unified temporal logic ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Compositional reasoning using intervals and time reversal ⋮ Verifying safety critical task scheduling systems in PPTL axiom system ⋮ A formal proof of the deadline driven scheduler in PPTL axiomatic system ⋮ Index set expressions can represent temporal logic formulas ⋮ Some Fixed-Point Issues in PPTL ⋮ PPTL specification mining based on LNFG
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Operational semantics of Framed Tempura
- Framed temporal logic programming
- A decision procedure for propositional projection temporal logic with infinite models
- A lattice-theoretical fixpoint theorem and its applications
- Temporal logic can be more expressive
- Automated Theorem Proving: After 25 Years
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
This page was built for publication: A complete proof system for propositional projection temporal logic
