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
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/}
}
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/