# zbMATH — the first resource for mathematics

Unification and admissible rules for paraconsistent minimal Johanssons’ logic J and positive intuitionistic logic $$\mathbf{IPC}^+$$. (English) Zbl 1323.03029
Summary: We study unification problem and problem of admissibility for inference rules in minimal Johanssons’ logic J and positive intuitionistic logic $$\mathrm{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 $$\mathrm{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.

##### MSC:
 03B53 Paraconsistent logics 03B25 Decidability of theories and sets of sentences 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: