Unification and admissible rules for paraconsistent minimal Johanssonsʼ logic J and positive intuitionistic logic ${\mathbf{IPC}}^{+}$

Abstract

We study unification problem and problem of admissibility for inference rules in minimal Johanssonsʼ logic J and positive intuitionistic logic ${\mathbf{IPC}}^{+}$. This paper proves that the problem of admissibility for inference rules with coefficients (parameters) (as well as plain ones – without parameters) is decidable for the paraconsistent minimal Johanssonsʼ logic J and the positive intuitionistic logic ${\mathbf{IPC}}^{+}$. Using obtained technique we show also that the unification problem for these logics is also decidable: we offer algorithms which compute complete sets of unifiers for any unifiable formula. Checking just unifiability of formulas with coefficients also works via verification of admissibility.