Journal of Symbolic Logic 57 (3):912-923 (1992)

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 constructed 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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275439
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 68,975
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Unification in Linear Temporal Logic LTL.Sergey Babenyshev & Vladimir Rybakov - 2011 - Annals of Pure and Applied Logic 162 (12):991-1000.

View all 24 citations / Add more citations

Similar books and articles


Added to PP index

Total views
215 ( #52,092 of 2,498,264 )

Recent downloads (6 months)
1 ( #426,910 of 2,498,264 )

How can I increase my downloads?


My notes