A decision procedure and complete axiomatization for projection temporal logic

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

zbMATH Keywords

axiomatizationdecision procedureprojection temporal logiclabeled normal form graph

Mathematics Subject Classification ID

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

• MSVL

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