A new rule for LTL tableaux
From MaRDI portal
Publication:5015285
zbMATH Open1478.03030arXiv1609.04102MaRDI QIDQ5015285FDOQ5015285
Authors:
Publication date: 7 December 2021
Full work available at URL: https://arxiv.org/abs/1609.04102
Recommendations
Cites Work
- Implementing a fair monodic temporal logic prover
- Title not available (Why is that?)
- Title not available (Why is that?)
- The temporal logic of branching time
- Cut-free sequent systems for temporal logic
- Reasoning about infinite computations
- Title not available (Why is that?)
- Systematic semantic tableaux for PLTL
- Title not available (Why is that?)
- Efficient loop-check for backward proof search in some non-classical propositional logics
- A PLTL-prover based on labelled superposition with partial model guidance
- Two loop detection mechanisms: a comparison
- Mathematical Logic for Computer Science
- Title not available (Why is that?)
Cited In (13)
- Title not available (Why is that?)
- Systematic semantic tableaux for PLTL
- A one-pass tree-shaped tableau for LTL+past
- One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
- SAT meets tableaux for linear temporal logic satisfiability
- Theorem proving for pointwise metric temporal logic over the naturals via translations
- A One-Pass Tree-Shaped Tableau for Defeasible LTL
- Labelled tableaux for propositional linear time logic over finite frames
- Title not available (Why is that?)
- A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
- The saturated tableaux for linear miniscope Horn-like temporal logic
- And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL
- Title not available (Why is that?)
Uses Software
This page was built for publication: A new rule for LTL tableaux
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5015285)
