Сибирский федеральный университет

Тип публикации: статья из журнала

Год издания: 2013

Идентификатор DOI: 10.1093/jigpal/jzs015

Ключевые слова: intuitionistic logic, unification, complete set of unifiers, admissible rules

Аннотация: The article solves the generalized unification problem for the intuitionistic logic Int. This problem concerns unification of formulas with coefficients (i.e. meta-variables). Coefficients are propositional letters, which are logical constants, i.e. any unifier lets them intact. We find an algorithm constructing a finite complete set of unifiers for any unifiable formula. In terms of algebraic logic, we solve the problem of finding solutions for equations in the free pseudo-boolean algebra in the signature extended by constants for free variables. We construct an algorithm recognizing formulas with coefficients, which are unifiable in Int, and then computing a finite complete set of unifiers (so, any unifier is a substitutional example of an one from this set). So, in particular, we show that generalized unification problem (for formulas with coefficients) in Int is of finitary type. In the concluding section, we show how to transfer these results to the super-intuitionistic logic KC (the logic of the law of the excluded middle).

Журнал: LOGIC JOURNAL OF THE IGPL

Выпуск журнала: Vol. 21, Is. 2

Номера страниц: 187-198

ISSN журнала: 13670751

Место издания: OXFORD

Издатель: OXFORD UNIV PRESS

• Rybakov V.V. (Institute of Mathematics,Siberian Federal University)

• Web of Science Core Collection
• Scopus
• Ядро РИНЦ (eLIBRARY.RU)