A decision procedure and complete axiomatization for projection temporal logic
From MaRDI portal
Publication:1986563
DOI10.1016/j.tcs.2017.09.026zbMath1506.03070OpenAlexW2760114350MaRDI QIDQ1986563
Xinfeng Shu, Zhenhua Duan, Hongwei David Du
Publication date: 8 April 2020
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2017.09.026
Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Formalization of mathematics in connection with theorem provers (68V20)
Related Items
Efficient decision procedure for propositional projection temporal logic ⋮ A sound and complete proof system for a unified temporal logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A mechanism of function calls in MSVL
- A cylinder computation model for many-core parallel computing
- A complete proof system for propositional projection temporal logic
- A practical decision procedure for propositional projection temporal logic with infinite models
- 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
- Incompleteness of first-order temporal logic with until
- Completing the temporal picture
- Duration calculus. A formal approach to real-time systems.
- Expressiveness of propositional projection temporal logic with star
- Framed temporal logic programming
- A decision procedure for propositional projection temporal logic with infinite models
- Axiomatising first-order temporal logic: Until and since over linear time
- Extending MSVL with Semaphore
- A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time
- $$2^5$$ Years of Model Checking
- A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time
- Corrigendum: Soundness and Completeness of an Axiom System for Program Verification
- Propositional temporal logics: decidability and completeness
- A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
- Complete Proof System for QPTL
- A Complete Proof System for First-order Interval Temporal Logic with Projection
- Logic Programming
- Depth-First Search and Linear Graph Algorithms
- A light-weight integration of automated and interactive theorem proving