Тип публикации: статья из журнала
Год издания: 1992
Идентификатор DOI: 10.2307/2275439
Аннотация: An algorithm recognizing admissibility of inference rules in generalized form (rules of inference with parameters or metavariables) in the intuitionistic calculus H and, in particular, also in the usual form without parameters, is presented. This algorithm is obtained by means of special intuitionistic Kripke models, which are consПоказать полностьюtructed for a given inference rule. Thus, in particular. the direct solution by intuitionistic techniques of Friedman's problem is found. As a corollary an algorithm for the recognition of the solvability of logical equations in H and for constructing some solutions for solvable equations is obtained. A semantic criterion for admissibility in H is constructed.
Журнал: JOURNAL OF SYMBOLIC LOGIC
Выпуск журнала: Vol. 57, Is. 3
Номера страниц: 912-923
ISSN журнала: 00224812
Место издания: CHAMPAIGN
Издатель: ASSN SYMBOLIC LOGIC INC