Cut-free singlepass tableaux for the logic of common knowledge, Workshop on Agents and Deduction at TABLEAUX'07, 2007. ,
Modal satisfiability via SMT solving, Software, Services, and Systems -Essays Dedicated to Martin Wirsing, pp.30-45, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01127966
Predicting learnt clauses quality in modern SAT solvers, Proc. of IJCAI'09, pp.399-404, 2009. ,
A Benchmark Method for the Propositional Modal Logics K, KT, S4, J. Autom. Reasoning, vol.24, issue.3, pp.297-317, 2000. ,
Knowledge compilation in the modal logic S5, Proc. of AAAI'10, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00624482
Graph-based algorithms for boolean function manipulation, IEEE Trans. Computers, vol.35, issue.8, pp.677-691, 1986. ,
, Reasoning About Knowledge, 1995.
An Intuitionistic Modal Logic with Applications to the Formal Verification of Hardware, Proc. of CSL'94, pp.354-368, 1994. ,
Modality and databases, Proc. of TABLEAUX'00, pp.19-39, 2000. ,
LoTREC: Logical Tableaux Research Engineering Companion, Proc. of TABLEAUX'05, pp.318-322, 2005. ,
Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m), Inf. Comput, vol.162, issue.1-2, pp.158-178, 2000. ,
System description: *SAT: A platform for the development of modal decision procedures, Proc. of CADE'00, pp.291-296, 2000. ,
A subset-matching size-bounded cache for testing satisfiability in modal logics, Ann. Math. Artif. Intell, vol.33, issue.1, pp.39-67, 2001. ,
SAT vs. Translation based decision procedures for modal logics: a comparative evaluation, Journal of Applied Non-Classical Logics, vol.10, issue.2, pp.145-172, 2000. ,
The sat-based approach for classical modal logics, Proc. of AI*IA'99, pp.95-106, 1999. ,
SAT-Based Decision Procedures for Classical Modal Logics, J. Autom. Reasoning, vol.28, issue.2, pp.143-171, 2002. ,
Spartacus: A tableau prover for hybrid logic, Electr. Notes Theor. Comput. Sci, vol.262, pp.127-139, 2010. ,
The intractability of resolution, Theoretical Computer Science, vol.39, issue.0, pp.297-308, 1985. ,
Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic, Proc. of IJCAI'07, pp.2306-2311, 2007. ,
InKreSAT: Modal Reasoning via Incremental Reduction to SAT, Proc. of CADE'13, pp.436-442, 2010. ,
The Computational Complexity of Provability in Systems of Modal Propositional Logic, SIAM J. Comput, vol.6, issue.3, pp.467-480, 1977. ,
A modal logic of epistemic games, Games, vol.1, issue.4, pp.478-526, 2010. ,
Design and results of TANCS-2000 non-classical (modal) systems comparison, Proc. of Tableaux'00, pp.52-56, 2000. ,
Design and results of the tableaux-99 non-classical (modal) systems comparison, Proc. of Tableaux'99, pp.14-18, 1999. ,
Single step tableaux for modal logics: Methodology, computations, algorithms, Journal of Autom, vol.24, issue.3, pp.319-364, 2000. ,
Efficient Representations for the Modal Logic S5, Proc. of IJCAI'16, pp.1223-1229, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01311642
A new general method to generate random modal formulae for testing decision procedures, J. Artif. Intell. Res, vol.18, pp.351-389, 2003. ,
Handbook of Modal Logic, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00580143
Handbook of Automated Reasoning (in 2 volumes), 2001. ,
SAT Techniques for Modal and Description Logics, Handbook of Satisfiability, vol.185, pp.781-824, 2009. ,
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability, JAIR, vol.35, issue.1, p.343, 2009. ,
Sat-based decision procedures for normal modal logics: A theoretical framework, Proc. of AIMSA'98, pp.377-388, 1998. ,
The Tableau Prover Generator MetTeL2, Proc. of JELIA'12, pp.492-495, 2012. ,
On the Complexity of Derivation in Propositional Calculus, pp.466-483, 1983. ,
Distributed control flow with classical modal logic, Proc. of CSL'05, pp.51-69, 2005. ,
SPASS version 3.5, Proc. of CADE'09, pp.140-145, 2009. ,