Rewrite rules for \(\mathrm{CTL}^\ast\)
type: Item
instance of: scholarly article
title: Rewrite rules for \(\mathrm{CTL}^\ast\)
zbMATH Open document ID: 1436.03124
author: John Christopher McCabe-Dansted
author: Mark Alexander Reynolds
published in: Journal of Applied Logic
publication date: 2017-03-30T00:00:00Z
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 6698102
zbMATH Keywords: rewrite
zbMATH Keywords: verification
zbMATH Keywords: non-local logic
zbMATH Keywords: tableau
zbMATH Keywords: bundled logic
zbMATH Keywords: \(\mathrm{CTL}\)
describes a project that uses: AProVE
describes a project that uses: CiME
describes a project that uses: Waldmeister
MaRDI profile type: Publication
full work available at URL: j.jal.2016.12.003
OpenAlex ID: W2565989685
cites work: On Non-local Propositional and Weak Monodic Quantified CTL*
cites work: Logic and time
cites work: Q5389068
cites work: Q4808748
cites work: Using branching time temporal logic to synthesize synchronization skeletons
cites work: Decision procedures and expressiveness in the temporal logic of branching time
cites work: Deciding full branching time logic
cites work: Propositional dynamic logic of regular programs
cites work: A Decision Procedure for CTL* Based on Tableaux and Automata
cites work: Q3408862
cites work: Rewrite method for theorem proving in first order theory with equality
cites work: A refutational approach to geometry theorem proving
cites work: Q5581665
cites work: A rooted tableau for \(\mathrm{BCTL}^*\)
cites work: An axiomatization of full computation tree logic
cites work: Axioms for Branching Time
cites work: A Tableau for Bundled CTL
cites work: A tableau-based decision procedure for CTL\(^*\)
cites work: Q4353561
cites work: Branching-time logic with quantification over branches: The point of view of modal logic
DOI: 10.1016/J.JAL.2016.12.003
description: scientific article; zbMATH DE number 6698102