Deciding ATL^* satisfiability by tableaux

DOI10.1007/978-3-319-21401-6_14MaRDI QIDQ3454093zbMATH OpenOpenAlexFDO

Authors Amélie David

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-21401-6_14

zbMATH Keywords

\(\mathsf {ATL}^*\)alternating-time temporal logicautomated theorem proversatisfiabilitytableaux

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• Optimal tableau method for constructive satisfiability testing and model synthesis in the alternating-time temporal logic \(\mathrm{ATL}^+\)
• TATL: Implementation of ATL Tableau-Based Decision Procedure
• Tableau-based decision procedures for logics of strategic ability in multiagent systems
• A tableau-based decision procedure for CTL^*

Cites work

• \(\mathcal{EL}\)-ifying ontologies
• A faster tableau for \(\mathrm{CTL}^{\ast}\)
• Alternating-time temporal logic
• ATL* Satisfiability Is 2EXPTIME-Complete
• Deciding full branching time logic
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• Mixed methods for fourth-order elliptic and parabolic problems using radial basis functions
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+

Cited in

(16)

• Minimisation of \(\mathrm{ATL}^*\) models
• TATL
• Complexity of finite-variable fragments of propositional temporal and modal logics of computation
• Alternating-time temporal logic ATL with finitely bounded semantics
• Tableau method and NEXPTIME-completeness of DEL-sequents
• TATL: Implementation of ATL Tableau-Based Decision Procedure
• Tableau-based decision procedures for logics of strategic ability in multiagent systems
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• A tableau for bundled strategies
• ATL* Satisfiability Is 2EXPTIME-Complete
• Tableau-Based Procedure for Deciding Satisfiability in the Full Coalitional Multiagent Epistemic Logic
• A faster tableau for \(\mathrm{CTL}^{\ast}\)
• Optimal tableau method for constructive satisfiability testing and model synthesis in the alternating-time temporal logic \(\mathrm{ATL}^+\)
• Logics in Artificial Intelligence
• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
• COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)

This page was built for publication: Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux

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