|
Sibirskie Èlektronnye Matematicheskie Izvestiya [Siberian Electronic Mathematical Reports], 2014, Volume 11, Pages 434–443
(Mi semr498)
|
|
|
|
This article is cited in 1 scientific paper (total in 1 paper)
Mathematical logic, algebra and number theory
Unification Problem in Nelson's Logic $\mathbf{N4}$
S. P. Odintsova, V. V. Rybakovb a Sobolev Institute of Mathematics, pr. Koptyuga, 4, 630090, Novosibirsk, Russia
b School of Computing, Mathematics and DT, Manchester Metropolitan University, John Dalton Building, Chester Street,
Manchester M1 5GD, U.K.
Abstract:
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, unification, complete sets of unifiers, decidability, Vorob'ev translation.
Received January 16, 2014, published June 3, 2014
Citation:
S. P. Odintsov, V. V. Rybakov, “Unification Problem in Nelson's Logic $\mathbf{N4}$”, Sib. Èlektron. Mat. Izv., 11 (2014), 434–443
Linking options:
https://www.mathnet.ru/eng/semr498 https://www.mathnet.ru/eng/semr/v11/p434
|
Statistics & downloads: |
Abstract page: | 220 | Full-text PDF : | 76 | References: | 87 |
|