MC Logics and Modal Logics

A special class of Multi-Context systems called hierarchical meta-logics has been proved to be equivalent to normal modal logics. This theoretical results has influenced the development of a class of decision procedures for normal modal logics.

Hierarchical meta-logics [introduced in F. Giunchiglia and L. Serafini, Multi-language Hierarchical Logics (or: How we can do without modal logics)] are composed of a (possibly infinite) chain of contexts, each one containing a propositional meta-theory of the context below. Two adjacent contexts are connected by the bridge rules Rup and rdw, also called reflection rules.

Bounded modal logic (i.e., modal logics with a bounded number of nesting of modal operators) can be reconstructed with a hierarchical meta-logic with a finite chain of contexts, while normal modal logic K is reconstructed with an infinite chain of contexts. Generalizing this result, Multi-modal K can be reconstructed in a Hierarchical meta-logic with with an (infinite) tree of contexts, where each context contains a propositional meta-theory of all its children contexts.

Reasoning (= deduction) in hierarchical meta-logics goes up and down through the contexts of the chain. In principle the navigation path that one have to follow in order to prove a theorem is unbound and can contain cycles. However, in the proof theoretical paper (L. Serafini and F. Giunchiglia, ML Systems: A Proof Theory for Contexts), we have shown that any deduction in a hierarchical meta-logic can be reduced to a normal form, where the navigation path is bound and without cycles. Intuitively, a normal form deduction of a theorem in a context ii, reasons in the contexts below ii.

Hierarchical meta-logic and their normal forms have strongly influenced the SAT decision procedure described in [E. Giunchiglia, F. Giunchiglia, and A. Tacchella, SAT-Based Decision Procedures for Classical Modal Logics].

Relevant Publications

L. Serafini and F. Giunchiglia
ML Systems: A Proof Theory for Contexts
Journal of Logic, Language and Information Spring 2002, Volume 11, Issue 2 pp. 471-518. (pdf)
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)
E. Giunchiglia, F. Giunchiglia, and A. Tacchella
SAT-Based Decision Procedures for Classical Modal Logics
Journal of Automated Reasoning - Special Issue on SAT'2000. (
ps)
F. Giunchiglia and L. Serafini
Multilanguage Hierarchical Logics (or: How we can do without modal logics)
Artificial Intelligence, 65:29-70, 1994. (pdf)

 

Web mastering: Alessandro Tomasi
Last Update: February 2003