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.
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 PublicationsL. Serafini and F. Giunchiglia
|