Тип публикации: статья из журнала
Год издания: 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 sПоказать полностьюet 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