A new rule for LTL tableaux

MaRDI QIDQ5015285zbMATH OpenFDO

Authors

Publication date 7 December 2021

Full work available at URL https://arxiv.org/abs/1609.04102, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF2016.20

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 7445165
• Systematic semantic tableaux for PLTL
• Labelled tableaux for propositional linear time logic over finite frames
• A one-pass tree-shaped tableau for LTL+past
• A tableau-based decision procedure for CTL^*

Cites work

• A PLTL-prover based on labelled superposition with partial model guidance
• Cut-free sequent systems for temporal logic
• Efficient loop-check for backward proof search in some non-classical propositional logics
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 2102740 (Why is no real title available?)
• scientific article; zbMATH DE number 814821 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• Implementing a fair monodic temporal logic prover
• Mathematical Logic for Computer Science
• Reasoning about infinite computations
• Systematic semantic tableaux for PLTL
• The temporal logic of branching time
• Two loop detection mechanisms: a comparison

Cited in

(15)

• The saturated tableaux for linear miniscope Horn-like temporal logic
• One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
• A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
• Theorem proving for pointwise metric temporal logic over the naturals via translations
• Labelled tableaux for propositional linear time logic over finite frames
• Systematic semantic tableaux for PLTL
• And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL
• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• One-pass and tree-shaped tableau systems for \(\mathrm{TPTL}\) and \(\mathrm{TPTL}_b+\mathrm{Past}\)
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 1305046 (Why is no real title available?)
• scientific article; zbMATH DE number 980417 (Why is no real title available?)
• A one-pass tree-shaped tableau for LTL+past
• A One-Pass Tree-Shaped Tableau for Defeasible LTL
• SAT meets tableaux for linear temporal logic satisfiability

Describes a project that uses

Uses Software

• Aalta
• TRP++
• TSPASS
• NuSMV
• Leviathan
• TTM

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)