@article { author = {Ghilardi, S. and Lenzi, G.}, title = {Unification in lax logic}, journal = {Journal of Algebraic Hyperstructures and Logical Algebras}, volume = {3}, number = {1}, pages = {61-75}, year = {2022}, publisher = {University of Hatef (Hatef College University)}, issn = {2676-6000}, eissn = {2676-6019}, doi = {10.52547/HATEF.JAHLA.3.1.6}, abstract = {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.  }, keywords = {Nuclei,lax logic,unification theory,admissible inference rules}, url = {https://jahla.hatef.ac.ir/article_138458.html}, eprint = {https://jahla.hatef.ac.ir/article_138458_9502eef4201eff01e073b82589e6f118.pdf} }