TATL: Implementation of ATL Tableau-Based Decision Procedure

DOI10.1007/978-3-642-40537-2_10MaRDI QIDQ2851937zbMATH OpenOpenAlexFDO

Authors Amélie David

Publication date 4 October 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-40537-2_10

zbMATH Keywords

alternating-time temporal logictableauxtheorem prover

Mathematics Subject Classification ID

Temporal logic (03B44)

Recommendations

• A tableau-based decision procedure for CTL^*
• Tableau-based Decision Procedures for Hybrid Logic
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• An on-the-fly tableau-based decision procedure for PDL-satisfiability
• scientific article; zbMATH DE number 7085031
• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
• Implementing semantic tableaux
• A tableaux-based decision procedure for multi-parameter propositional schemata
• Decision tables and decision algorithms

Cited in

(6)

• TATL
• Tableau-based decision procedures for logics of strategic ability in multiagent systems
• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• Ordered resolution for coalition logic
• Optimal tableau method for constructive satisfiability testing and model synthesis in the alternating-time temporal logic \(\mathrm{ATL}^+\)
• COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)

This page was built for publication: TATL: Implementation of ATL Tableau-Based Decision Procedure

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2851937)