, Modal Satisfiability via SMT Solving. Dans Software, Services, and Systems, pp.30-45, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01127966
Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction, Proc. of SAT'13, pp.309-317, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00845496
, A Benchmark Method for the Propositional Modal Logics K, KT, S4. JAR, vol.24, pp.297-317, 2000.
Hans van Maaren et Toby Walsh (rédacteurs): Handbook of Satisfiability, tome 185 de Frontiers in Artificial Intelligence and Applications, pp.978-979, 2009. ,
Handbook of Modal Logic, tome 3, pp.978-0444516909, 2006. ,
Modal Logic: An Introduction ,
CounterExample-Guided Abstraction Refinement For Symbolic Model Checking, J. of the ACM, vol.50, issue.5, pp.752-794, 2003. ,
, An Extensible SAT-solver
, Dans Proc. of SAT'03, pp.502-518, 2003.
A General Filtration Method For Modal Logics, Journal of Philosophical Logic, vol.1, issue.1, pp.29-34, 1972. ,
SAT-Based Decision Procedures for Classical Modal Logics, JAR, vol.28, issue.2, pp.143-171, 2002. ,
Implementing Tableau Calculi Using BDDs: BDDTab System Description, Proc. of IJCAR'14, pp.337-343, 2014. ,
, Spartacus: A Tableau Prover for Hybrid Logic. ENTCS, vol.262, pp.127-139, 2010.
, Computational Modal Logic. Studies in Logic and Practical Reasoning, vol.3, pp.181-245, 2007.
Solving QBF with CounterExample Guided Refinement, Art. Int, vol.234, pp.1-25, 2016. ,
,
InKreSAT: Modal Reasoning via Incremental Reduction to SAT, Proc. of CADE'13, pp.436-442, 2013. ,
First-Order Theorem Proving and Vampire, Proc. of CAV'13, pp.1-35, 2013. ,
A Completeness Theorem in Modal Logic, J. Symb. Log, vol.24, issue.1, pp.1-14, 1959. ,
Tiago de Lima et Valentin Montmirail: A Recursive Shortcut for CE-GAR: Application To The Modal Logic K Satisfiability Problem, Proc. of IJCAI'17, 2017. ,
Tiago de Lima et Valentin Montmirail: A SAT-Based Approach For PSPACE Modal Logics, Proc. of KR'18, pp.651-652, 2018. ,
An Improved Decision-DNNF Compiler, Proc. of IJCAI'17, pp.667-673, 2017. ,
Core Equivalence in Economy for Modal Logic, Proc. of ICCS'03, Part II, pp.74-83, 2003. ,
A Resolution-Based Prover for Multimodal K, Proc. of IJCAR'16, pp.406-415, 2016. ,
On Compiling CNF into Decision-DNNF, Proc. of CP'14, pp.42-57, 2014. ,
, , vol.4, pp.75-97
, , vol.4, pp.483-504
rédac-teurs): Handbook of Automated Reasoning, tome 1, 2001. ,
Completeness and correspondence in the first and second order semantics for modal logic, Proc. of the 3rd Scandinavian Logic Sumposium, 1973. ,
Using SAT in QBF, Proc. of CP'05, pp.578-592, 2005. ,
Kautz et Toniann Pitassi: Combining Component Caching and Clause Learning for E?ective Model Counting, Proc. of SAT'04, 2004. ,
New Upper Bounds for Satisfiability in Modal Logics the Casestudy of Modal K, 1997. ,
, SAT Techniques for Modal and Description Logics, vol.4, pp.978-979
, Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. JAIR, vol.35, pp.343-389, 2009.
Marc: sharpSAT -Counting Models with Advanced Component Caching and Implicit BCP, Proc. of SAT'06, pp.424-429, 2006. ,
Iván Martínez Ruiz et José Ramón Enrique Arrazola-Ramírez: On Automatic Theorem Proving with ML, Proc. of MI-CAI'14, pp.231-236, 2014. ,
FaCT++ Description Logic Reasoner: System Description, Proc. of IJCAR'06, pp.292-297, 2006. ,
On the Complexity of Derivation in Propositional Calculus, pp.466-483, 1983. ,
Modal Logic For Open Minds, tome 1. Center for the Study of Language and Inf, pp.978-1575865980, 2010. ,