OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

About the unification type of modal logics between KB and KTB

Balbiani, Philippe and Gencer, Cigdem About the unification type of modal logics between KB and KTB. (2019) Studia Logica. ISSN 0039-3215

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/s11225-019-09883-0


The unification problem in a normal modal logic is to determine, given a formula φ, whether there exists a substitution σ such that σ(φ) is in that logic. In that case, σ is a unifier of φ. We shall say that a set of unifiers of a unifiable formula φ is minimal complete if for all unifiers σ of φ, there exists a unifier τ of φ in that set such that τ is more general than σ and for all σ,τ in that set, σ≠τ, neither σ is more general than τ, nor τ is more general than σ. When a unifiable formula has no minimal complete set of unifiers, the formula is nullary. We usually distinguish between elementary unification and unification with parameters. In elementary unification, all variables are likely to be replaced by formulas when one applies a substitution. In unification with parameters, some variables—called parameters—remain unchanged. In this paper, we prove that normal modal logics KB, KDB and KTB as well as infinitely many normal modal logics between KDB and KTB possess nullary formulas for unification with parameters.

Item Type:Article
HAL Id:hal-02903127
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Other partners > İstanbul Aydin Üniversitesi - IAU (TURKEY)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:20 Jul 2020 14:40

Repository Staff Only: item control page