Deciding $$\mathsf {ATL^*}$$ Satisfiability by Tableaux

DOI10.1007/978-3-319-21401-6_14zbMath1465.68278OpenAlexW1454650980MaRDI QIDQ3454093

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

tableauxsatisfiabilityautomated theorem proveralternating-time temporal logic\(\mathsf {ATL}^*\)

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)

Related Items (3)

Complexity of finite-variable fragments of propositional temporal and modal logics of computation ⋮ COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description) ⋮ TATL

Cites Work

• Unnamed Item
• Unnamed Item
• 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+
• $\mathcal{EL}$ -ifying Ontologies
• Alternating-time temporal logic
• ATL* Satisfiability Is 2EXPTIME-Complete
• Deciding full branching time logic

This page was built for publication: Deciding $$\mathsf {ATL^*}$$ Satisfiability by Tableaux