In this paper, we focus on the intuitionistic propositional logic extended with a local operator [22] (also called nucleus [21]); such logic is commonly named lax logic after [9]. We prove that unification is finitary in this logic and supply algorithms for computing a basis of unifiers and for recognizing admissibility of inference rules, following analogous known results for intuitionistic logic.
Ghilardi, S., Lenzi, G. (2022). Unification in lax logic. Journal of Algebraic Hyperstructures and Logical Algebras, 3(1), 61-75. doi: 10.52547/HATEF.JAHLA.3.1.6
MLA
S. Ghilardi; G. Lenzi. "Unification in lax logic". Journal of Algebraic Hyperstructures and Logical Algebras, 3, 1, 2022, 61-75. doi: 10.52547/HATEF.JAHLA.3.1.6
HARVARD
Ghilardi, S., Lenzi, G. (2022). 'Unification in lax logic', Journal of Algebraic Hyperstructures and Logical Algebras, 3(1), pp. 61-75. doi: 10.52547/HATEF.JAHLA.3.1.6
VANCOUVER
Ghilardi, S., Lenzi, G. Unification in lax logic. Journal of Algebraic Hyperstructures and Logical Algebras, 2022; 3(1): 61-75. doi: 10.52547/HATEF.JAHLA.3.1.6
)