Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6424781 | Annals of Pure and Applied Logic | 2013 | 14 Pages |
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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Sergei Odintsov, Vladimir Rybakov,