Unification Problem in Nelson's Logic $\mathbf{N4}$
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 11 (2014), pp. 434-443

Voir la notice de l'article provenant de la source Math-Net.Ru

We consider the unification problem for formulas with coeffi-cients in the Nelson's paraconsitent logic $\mathbf{N4}$. By presence coefficients (parameters) the problem is quite not trivial and challenging (yet what makes the problem for $\mathbf{N4}$ to be peculiar is missing of replacement equivalents rule in this logic). It is shown that the unification problem in $\mathbf{N4}$ is decidable for $\sim$-free formulas. We also show that there is an algorithm which computes finite complete sets of unifiers (so to say — all best unifiers) for unifiable in $\mathbf{N4}$ $\sim$-free formulas (i.e. any unifier is equivalent to a substitutional example of a unifier from this complete set). Though the unification problem for all formulas (not $\sim$-free formulas) remains open.
Keywords: Nelson's logic, strong negation, complete sets of unifiers, decidability, Vorob'ev translation.
Mots-clés : unification
@article{SEMR_2014_11_a13,
     author = {S. P. Odintsov and V. V. Rybakov},
     title = {Unification {Problem}  in {Nelson's} {Logic} $\mathbf{N4}$},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {434--443},
     publisher = {mathdoc},
     volume = {11},
     year = {2014},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2014_11_a13/}
}
TY  - JOUR
AU  - S. P. Odintsov
AU  - V. V. Rybakov
TI  - Unification Problem  in Nelson's Logic $\mathbf{N4}$
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2014
SP  - 434
EP  - 443
VL  - 11
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2014_11_a13/
LA  - en
ID  - SEMR_2014_11_a13
ER  - 
%0 Journal Article
%A S. P. Odintsov
%A V. V. Rybakov
%T Unification Problem  in Nelson's Logic $\mathbf{N4}$
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2014
%P 434-443
%V 11
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2014_11_a13/
%G en
%F SEMR_2014_11_a13
S. P. Odintsov; V. V. Rybakov. Unification Problem  in Nelson's Logic $\mathbf{N4}$. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 11 (2014), pp. 434-443. http://geodesic.mathdoc.fr/item/SEMR_2014_11_a13/