We characterize provability in intuitionistic predicate logic in terms of derivation skeletons and constraints and study the problem of instantiations of a skeleton to valid derivations. We prove that for two different notions of a skeleton the problem is respectively polynomial and NP-complete. As an application of our technique, we demonstrate PSPACE-completeness of the prenex fragment of intuitionistic logic. We outline some applications of the proposed technique in automated reasoning.
CITATION STYLE
Voronkov, A. (1996). Proof-search in intuitionistic logic based on constraint satisfaction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1071, pp. 312–329). Springer Verlag. https://doi.org/10.1007/3-540-61208-4_20
Mendeley helps you to discover research relevant for your work.