Writing out unifiers for formulas with coefficients in intuitionistic logic

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

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

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

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

Аннотация: 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)

Вхождение в базы данных

Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.

Вы можете отметить интересные фрагменты текста, которые будут доступны по уникальной ссылке в адресной строке браузера.