Inference Procedures

This work is based on the fact that it is possible to define MC logics which are equivalent to the various normal and non normal modal logics. The second main intuition is to use propositional deciders (SAT) to reason inside each context. The result has been that of defining and implementing new deciders for various (modal) logics, which were orders of magnitude faster than the previous tableau-based decision procedures.

Relevant Publications

Enrico Giunchiglia, Fausto Giunchiglia and Armando Tacchella
SAT-Based Decision Procedures for Classical Modal Logics
January, 2005. (pdf)
Floris Roelofsen and Luciano Serafini
Satisfiability for Propositional Contexts
International Conference on the Principles of Knowledge Representation and Reasoning (KR-04), 2004. (pdf)
Serafini L. and Roelofsen F.
Complexity of contextual reasoning
National Conference on Artificial Intelligence (AAAI-04), 2004. (pdf)
Floris Roelofsen, Luciano Serafini and Alessandro Cimatti
Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems
European Conference on Artificial Intelligence (ECAI-04), 2004. (pdf)
Fausto Giunchiglia and Roberto Sebastiani
Building decision procedures for modal logics from propositional decision procedures - the case study of modal K(m)
Journal of Information and Computation. Vol 162 (1/2), pages. 158--178, October/November 2000, ©Academic Press. (ps)
Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani and Armando Tacchella
SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
Journal of Applied Non-Classical Logics, vol. 10, n. 2, 2000, pages 145--172. © Hermes International, Oxford. (ps)
Massimo Benerecetti, Fausto Giunchiglia and Luciano Serafini
Model Checking Multiagent Systems
Journal of Logic and Computation, Special Issue "Computational and Logical Aspects of Multi-Agent Systems", 8(3), 401-423, 1998. (ps)

 

Web mastering: Alessandro Tomasi
Last Update: January 2005