About the unification type of simple symmetric modal logics
Logic in Computer Science
2019-02-12 v1
Abstract
The unification problem in a normal modal logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. We shall say that a set of unifiers of a unifiable formula F is complete if for all unifiers s of F, there exists a unifier t of F in that set such that t is more general than s. When a unifiable formula has no minimal complete set of unifiers, the formula is nullary. In this paper, we prove that KB, KDB and KTB possess nullary formulas.
Cite
@article{arxiv.1902.03770,
title = {About the unification type of simple symmetric modal logics},
author = {Philippe Balbiani and Çiğdem Gencer},
journal= {arXiv preprint arXiv:1902.03770},
year = {2019}
}