Abstract
Let \(\varphi _{1},\ldots ,\varphi _{n}\) and \(\psi \) be some formulas.
Access provided by Autonomous University of Puebla. Download conference paper PDF
Similar content being viewed by others
Keywords
- Modal logics
- Unification problem
- Elementary unification
- Unification with constants
- Computability of unification
- Unification type
Let \(\varphi _{1},\ldots ,\varphi _{n}\) and \(\psi \) be some formulas. The figure \(\frac{\varphi _{1},\ldots ,\varphi _{n}}{\psi }\) is the inference rule which for all substitutions \(\sigma \), derives \(\sigma (\psi )\) from \(\sigma (\varphi _{1}),\ldots ,\sigma (\varphi _{n})\). It is admissible in a propositional logic L whenever for all substitutions \(\sigma \), \(\sigma (\psi )\in L\) if \(\sigma (\varphi _{1}),\ldots ,\sigma (\varphi _{n})\in L\). It is derivable in L whenever there is a derivation of \(\psi \) in L from the hypothesis \(\varphi _{1},\ldots ,\varphi _{n}\). It is evident that every derivable rule is also admissible. L is called structurally complete when the converse holds. Some propositional logics — such as Classical Propositional Logic — are structurally complete. Others — like Intuitionistic Propositional Logic — are not. See [14, Chap. 2]. When L is not structurally complete, owing to the importance of the admissibility problem in the mechanization of propositional logics, it is crucial to be able to recognize whether a given inference rule is admissible. The question of the existence of a decidable modal logic with an undecidable admissibility problem has been negatively answered by Wolter and Zakharyaschev [41] within the context of normal modal logics between K and K4 enriched with the universal modality — see also the pioneering article of Chagrov [13] for an earlier example of a decidable modal logic with an undecidable admissibility problem. In some other cases, for instance Intuitionistic Propositional Logic and transitive normal modal logics like K4, the question of the decidability of the admissibility problem has been positively answered by Rybakov [33,34,35]. See also [15, 25, 27, 28, 32]. The truth is that Rybakov’s decidability results are related to the fact that the propositional logics he has considered are finitary [22,23,24].
The finitariness character of a propositional logic L originates in its unification problem. The unification problem in L is to determine, given a formula \(\varphi \), whether there exists a substitution \(\sigma \) such that \(\sigma (\varphi )\) is in L. In that case, \(\sigma \) is a unifier of \(\varphi \). A formula \(\varphi \) is filtering if for all unifiers \(\sigma \) and \(\tau \) of \(\varphi \), there exists a unifier of \(\varphi \) which is more general than \(\sigma \) and \(\tau \). We shall say that a set of unifiers of a formula \(\varphi \) is complete if for all unifiers \(\sigma \) of \(\varphi \), there exists a unifier \(\tau \) of \(\varphi \) in that set such that \(\tau \) is more general than \(\sigma \). An important question is the following: when a formula is unifiable, has it a minimal complete set of unifiers? When the answer is “no”, the formula is nullary. When the answer is “yes”, the formula is either infinitary, or finitary, or unitary depending on the cardinalities of its minimal complete sets of unifiers. Filtering formulas are always unitary, or nullary. A propositional logic is called nullary if it possesses a nullary formula. Otherwise, it is called either infinitary, or finitary, or unitary depending on the types of its unifiable formulas. When every formula is filtering, the propositional logic is called filtering. See [3, 17, 26] for details. It is evident that if L is consistent then its unification problem can be reduced to its admissibility problem: a given formula \(\varphi \) possesses a unifier in L if and only if the inference rule \(\frac{\varphi }{\bot }\) is not admissible. Reciprocally, if L is unitary, or finitary and the elements of the minimal complete sets of unifiers given rise by its unifiable formulas can be computed then its admissibility problem can be reduced to its unification problem: a given inference rule \(\frac{\varphi _{1},\ldots ,\varphi _{n}}{\psi }\) is admissible in L if and only if either \(\varphi _{1}\wedge \ldots \wedge \varphi _{n}\) is not unifiable, or the substitutions that belong to a minimal complete set of unifiers of \(\varphi _{1}\wedge \ldots \wedge \varphi _{n}\) are unifiers of \(\psi \).
In accordance with their capacity to talk about relational structures, normal modal logics like epistemic logics, or temporal logics are playing a fundamental role in many applications. By virtue of its close relationships with the admissibility problem, the unification problem lies at the heart of their mechanization. For this reason, as advocated by Babenyshev et al. [7], investigations in the unification problem in normal modal logics can greatly contribute to the development of their applications. Regarding the unification problem in normal modal logics, we usually distinguish between elementary unification and unification with constants. In elementary unification, all variables are likely to be replaced by formulas when one applies a substitution. In unification with constants, some variables — called constants — remain unchanged. In normal modal logics extending KD, the elementary unification problem can be decided in nondeterministic polynomial time, seeing that one can easily decide whether a given variable-free formula is equivalent to \(\bot \), or is equivalent to \(\top \). In many transitive normal modal logics like K4, solving the elementary unification problem is more difficult. In some other normal modal logics like K, it is even unknown whether the elementary unification problem is decidable. As for the unification problem with constants, it is not known to be decidable even for a simple normal modal logic such as \(Alt_{1}\). The truth is that the unification problem with constants is only known to be decidable for a limited number of transitive normal modal logics like K4. In many cases, the decidability of the unification problem is a consequence of the decidability of the corresponding admissibility problem. See [23, 24, 29, 36,37,38,39,40] for details.
Concerning the unification types of normal modal logics, it is known that S5 is unitary [3], KT is nullary [8], KD is nullary [9], \(Alt_{1}\) is nullary [11], S4.3 is unitary [19], transitive normal modal logics like K4 are finitary [24] and K is nullary [30], though the nullariness character of KT and KD has only been obtained within the context of unification with constants. For some other normal modal logics such as the normal extensions of K4, they are filtering — therefore they are unitary, or nullary — if and only if they contain the modal translation of the weak law \(\lnot p\vee \lnot \lnot p\) of the excluded middle [26]. Taking a look at the literature about unification types in normal modal logics [3, 17, 26], one will quickly notice that much remains to be done. For instance, the types of symmetric normal modal logics like KB, KTB and KDB and the types of Church-Rosser normal modal logics like KG, KTG and KDG are unknown. Even the types of simple normal modal logics such as \(K+\Box ^{k}\bot \) are unknown when \(k\in \mathbb {N}\) is such that \(k\ge 2\). In his proof that K is nullary, Jer̆ábek [30] has taken the formula \((x\rightarrow \Box x)\) and has shown that it has no minimal complete set of unifiers. In this respect, he has mainly used the following properties of the modality \(\Box \): for all \(k,l\in \mathbb {N}\), if \((\Box ^{l}\bot \rightarrow \Box ^{k}\bot )\in K\) then \(l\le k\); for all formulas \(\psi \) and for all \(k\in \mathbb {N}\), if \((\psi \rightarrow \Box \psi )\in K\) and \(\deg (\psi )\le k\) then \(\psi \in K\), or \((\psi \rightarrow \Box ^{k}\bot )\in K\). Since for all \(k\in \mathbb {N}\), \(\lnot \Box ^{k}\bot \in KD\), therefore the adaptation of Jer̆ábek’s argument to KT and KD is not straightforward. It has been done in [8, 9] by taking the formula \((x\rightarrow p)\wedge (y\rightarrow q)\wedge (x\rightarrow \Box (q\rightarrow y))\wedge (y\rightarrow \Box (p\rightarrow x))\) in the case of KT and by taking the formula \((x\rightarrow p)\wedge (x\rightarrow \Box (p\rightarrow x))\) in the case of KD.
In this talk, we will give a survey of the results on unification in modal logic and we will present some of the open problems whose solution will have a great impact on the future of the area. After an introductory part about unification in equational theories, we will consider the case of Boolean unification [1, 31], we will study the unification problem in Intuitionistic Propositional Logic and transitive normal modal logics like K4 [21,22,23, 36, 37], we will introduce the notions of projective and transparent unifiers [16,17,18,19, 24] and we will define filtering unification [26]. Then, we will present the latest results obtained within the context of unification in description logics [2, 4, 5, 20] and in multimodal, tense and epistemic logics [6, 10, 12, 16].
Special acknowledgement is heartily granted to Çiğdem Gencer (Istanbul Aydın University, Turkey), Mojtaba Mojtahedi (Tehran University, Iran), Maryam Rostamigiv (Toulouse University, France) and Tinko Tinchev (Sofia University, Bulgaria) for their feedback: their useful suggestions have been essential for improving a preliminary versions of this talk.
References
Baader, F.: On the complexity of Boolean unification. Inf. Process. Lett. 67, 215–220 (1998)
Baader, F., Borgwardt, S., Morawska, B.: Extending unification in \(\cal{EL}\) towards general TBoxes. In: Brewka, G. et al. (eds.) Principles of Knowledge Representation and Reasoning, pp. 568–572. AAAI Press (2012)
Baader, F., Ghilardi, S.: Unification in modal and description logics. Log. J. IGPL 19, 705–730 (2011)
Baader, F., Morawska, B.: Unification in the description logic \(\cal{EL}\). In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 350–364. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02348-4_25
Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31, 277–305 (2001)
Babenyshev, S., Rybakov, V.: Unification in linear temporal logic \(LTL\). Ann. Pure Appl. Log. 162, 991–1000 (2011)
Babenyshev, S., Rybakov, V., Schmidt, R., Tishkovsky, D.: A tableau method for checking rule admissibility in \(S4\). Electron. Notes Theor. Comput. Sci. 262, 17–32 (2010)
Balbiani, P.: Remarks about the unification type of some non-symmetric non-transitive modal logics. Log. J. IGPL (2018, to appear)
Balbiani, P., Gencer, Ç.: \(KD\) is nullary. J. Appl. Non Class. Log. 27, 196–205 (2017)
Balbiani, P., Gencer, Ç.: Unification in epistemic logics. J. Appl. Non Class. Log. 27, 91–105 (2017)
Balbiani, P., Tinchev, T.: Unification in modal logic \(Alt_{1}\). In: Advances in Modal Logic, pp. 117–134. College Publications (2016)
Balbiani, P., Tinchev, T.: Elementary unification in modal logic \(KD45\). J. Appl. Log. IFCoLog J. Log. Appl. 5, 301–317 (2018)
Chagrov, A.: Decidable modal logic with undecidable admissibility problem. Algebra i Logika 31, 83–93 (1992)
Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997)
Cintula, P., Metcalfe, G.: Admissible rules in the implication-negation fragment of intuitionistic logic. Ann. Pure Appl. Log. 162, 162–171 (2010)
Dzik, W.: Unitary unification of \(S5\) modal logics and its extensions. Bull. Sect. Log. 32, 19–26 (2003)
Dzik, W.: Unification Types in Logic. Wydawnicto Uniwersytetu Slaskiego, Katowice (2007)
Dzik, W.: Remarks on projective unifiers. Bull. Sect. Log. 40, 37–46 (2011)
Dzik, W., Wojtylak, P.: Projective unification in modal logic. Log. J. IGPL 20, 121–153 (2012)
Fernández Gil, O.: Hybrid Unification in the Description Logic \(\cal{EL}\). Master thesis of Technische Universität Dresden (2012)
Gencer, Ç.: Description of modal logics inheriting admissible rules for \(K4\). Log. J. IGPL 10, 401–411 (2002)
Gencer, Ç., de Jongh, D.: Unifiability in extensions of \(K4\). Log. J. IGPL 17, 159–172 (2009)
Ghilardi, S.: Unification in intuitionistic logic. J. Symb. Log. 64, 859–880 (1999)
Ghilardi, S.: Best solving modal equations. Ann. Pure Appl. Log. 102, 183–198 (2000)
Ghilardi, S.: A resolution/tableaux algorithm for projective approximations in \(IPC\). Log. J. IGPL 10, 229–243 (2002)
Ghilardi, S., Sacchetti, L.: Filtering unification and most general unifiers in modal logic. J. Symb. Log. 69, 879–906 (2004)
Iemhoff, R.: On the admissible rules of intuitionistic propositional logic. J. Symb. Comput. 66, 281–294 (2001)
Iemhoff, R., Metcalfe, G.: Proof theory for admissible rules. Ann. Pure Appl. Log. 159, 171–186 (2009)
Jer̆ábek, E.: Complexity of admissible rules. Arch. Math. Log. 46, 73–92 (2007)
Jer̆ábek, E.: Blending margins: the modal logic \(K\) has nullary unification type. J. Log. Comput. 25, 1231–1240 (2015)
Martin, U., Nipkow, T.: Boolean unification – the story so far. J. Symb. Comput. 7, 275–293 (1989)
Rozière, P.: Règles admissibles en calcul propositionnel intuitionniste. Thesis of the University Paris VII (1993)
Rybakov, V.: A criterion for admissibility of rules in the model system \(S4\) and the intuitionistic logic. Algebra Log. 23, 369–384 (1984)
Rybakov, V.: Bases of admissible rules of the logics \(S4\) and \(Int\). Algebra Log. 24, 55–68 (1985)
Rybakov, V.: Admissibility of Logical Inference Rules. Elsevier, Amsterdam (1997)
Rybakov, V.: Construction of an explicit basis for rules admissible in modal system \(S4\). Math. Log. Q. 47, 441–446 (2001)
Rybakov, V., Gencer, Ç., Oner, T.: Description of modal logics inheriting admissible rules for \(S4\). Log. J. IGPL 7, 655–664 (1999)
Rybakov, V., Terziler, M., Gencer, Ç.: An essay on unification and inference rules for modal logics. Bull. Sect. Log. 28, 145–157 (1999)
Rybakov, V., Terziler, M., Gencer, Ç.: Unification and passive inference rules for modal logics. J. Appl. Non Class. Log. 10, 369–377 (2000)
Rybakov, V., Terziler, M., Gencer, Ç.: On self-admissible quasi-characterizing inference rules. Stud. Logica. 65, 417–428 (2000)
Wolter, F., Zakharyaschev, M.: Undecidability of the unification and admissibility problems for modal and description logics. ACM Trans. Comput. Log. 9, 25:1–25:20 (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer-Verlag GmbH Germany, part of Springer Nature
About this paper
Cite this paper
Balbiani, P. (2019). Unification in Modal Logic. In: Khan, M., Manuel, A. (eds) Logic and Its Applications. ICLA 2019. Lecture Notes in Computer Science(), vol 11600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-58771-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-662-58771-3_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-58770-6
Online ISBN: 978-3-662-58771-3
eBook Packages: Computer ScienceComputer Science (R0)