Symmetric blocking

DOI10.1016/J.TCS.2015.06.020MaRDI QIDQ897931zbMATH OpenOpenAlexFDO

Authors Carlos Areces, Ezequiel Orbe

Publication date 8 December 2015

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

Full work available at URL https://doi.org/10.1016/j.tcs.2015.06.020

zbMATH Keywords

symmetryevaluationmodal logicsblockingdetection

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Recommendations

• Dealing with Symmetries in Modal Tableaux
• Symmetries in modal logics
• Modal tableau systems with blocking and congruence closure
• Symmetries in modal logics
• Uniform and non uniform strategies for tableaux calculi for modal logics

Cites work

• scientific article; zbMATH DE number 67503 (Why is no real title available?)
• scientific article; zbMATH DE number 1348469 (Why is no real title available?)
• scientific article; zbMATH DE number 1946871 (Why is no real title available?)
• A benchmark method for the propositional modal logics K, KT, S4
• Dealing with Symmetries in Modal Tableaux
• Engineering an efficient canonical labeling tool for large and sparse graphs
• Exploiting symmetry in SMT problems
• HTab: a terminating tableaux system for hybrid logic
• Handbook of modal logic
• Hybrid tableaux for the difference modality
• Isomorphism of graphs of bounded valence can be tested in polynomial time
• Modal logic
• Optimizing description logic subsumption
• Short proofs for tricky formulas
• Symmetries in modal logics
• Tableau methods for modal and temporal logics
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Tractability through symmetries in propositional calculus

Cited in

(3)

• Symmetries in modal logics
• Symmetries in modal logics
• Modal tableau systems with blocking and congruence closure

Describes a project that uses

Uses Software

• HGen
• bliss
• HTab
• Spartacus
• FaCT++
• QBFLIB
• TPTP

This page was built for publication: Symmetric blocking

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