Tableau method and NEXPTIME-completeness of DEL-sequents

DOI10.1016/J.ENTCS.2011.10.003MaRDI QIDQ2825404zbMATH OpenOpenAlexWikidataFDO

Authors Guillaume Aucher, Bastien Maubert, François Schwarzentruber

Publication date 7 October 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2011.10.003

zbMATH Keywords

computational complexitydynamic epistemic logictableau method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logics of knowledge and belief (including belief change) (03B42) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Logic in artificial intelligence (68T27) Agent technology and artificial intelligence (68T42)

Recommendations

• Tableau methods for modal and temporal logics
• scientific article; zbMATH DE number 3937153
• A tableau construction for finite linear-time temporal logic
• Tableaux and restricted quantification for systems related to weak Kleene logic
• A tableau calculus for non-clausal maximum satisfiability
• Tableau method for residuated logic
• Synthetic completeness proofs for Seligman-style tableau systems
• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• A general tableau method for propositional interval temporal logics
• Completeness and termination for a Seligman-style tableau system

Cites work

• Algebra and sequent calculus for epistemic actions
• Automated Reasoning with Analytic Tableaux and Related Methods
• scientific article; zbMATH DE number 1048047 (Why is no real title available?)
• scientific article; zbMATH DE number 2149447 (Why is no real title available?)
• Logics for epistemic programs
• Tableaux for Public Announcement Logic
• Terminating tableaux for dynamic epistemic logics
• The logic of public announcements, common knowledge, and private suspicions

Cited in

(10)

• A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks
• Generalized DEL-Sequents
• Terminating tableaux for dynamic epistemic logics
• Tableaux for single-agent epistemic PDL with perfect recall and no miracles
• DEL-sequents for regression and epistemic planning
• Parameterized complexity results for a model of theory of mind based on dynamic epistemic logic
• On the computational complexity of model checking for dynamic epistemic logic with S5 models
• DEL-sequents for progression
• DEL-sequents for progression
• Logic for update products and steps into the past

Describes a project that uses

Uses Software

• LoTREC

This page was built for publication: Tableau method and NEXPTIME-completeness of DEL-sequents

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