Article ID Journal Published Year Pages File Type
6424781 Annals of Pure and Applied Logic 2013 14 Pages PDF
Abstract

We study unification problem and problem of admissibility for inference rules in minimal Johanssonsʼ logic J and positive intuitionistic logic 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 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.

Keywords
Related Topics
Physical Sciences and Engineering Mathematics Logic
Authors
, ,