A sound and complete proof system for a unified temporal logic
From MaRDI portal
Publication:2197533
DOI10.1016/j.tcs.2020.05.015zbMath1485.03045OpenAlexW3028347811MaRDI QIDQ2197533
Publication date: 1 September 2020
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2020.05.015
Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A complete proof system for propositional projection temporal logic
- A practical decision procedure for propositional projection temporal logic with infinite models
- A formal proof of the deadline driven scheduler in PPTL axiomatic system
- Completing the temporal picture
- A decision procedure and complete axiomatization for projection temporal logic
- A proof system for a unified temporal logic
- Index set expressions can represent temporal logic formulas
- Expressiveness of propositional projection temporal logic with star
- Framed temporal logic programming
- A decision procedure for propositional projection temporal logic with infinite models
- A lattice-theoretical fixpoint theorem and its applications
- A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time
- A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
- Complete Proof System for QPTL
- A light-weight integration of automated and interactive theorem proving
This page was built for publication: A sound and complete proof system for a unified temporal logic
