On the Mints Hierarchy in First-Order Intuitionistic Logic

DOI10.2168/LMCS-12(4:11)2016zbMath1445.03008MaRDI QIDQ5892381

Aleksy Schubert, Konrad Zdanowski, Paweł Urzyczyn

Publication date: 11 April 2017

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

complexityautomataintuitionistic logicMints hierarchy

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (3)

Practical Proof Search for Coq by Type Inhabitation ⋮ First-order Answer Set Programming as Constructive Proof Search ⋮ The existential fragment of second-order propositional intuitionistic logic is undecidable

Uses Software

• Coq
• Agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Syntactic preservation theorems for intuitionistic predicate logic
• The foundation of a generic theorem prover
• Eigenvariables, bracketing and the decidability of positive minimal predicate logic
• Sovability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers
• On the first-order prefix hierarchy
• The Complexity of Inhabitation with Explicit Intersection
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae
• The Inhabitation Problem for Rank Two Intersection Types
• Inhabitation of Low-Rank Intersection Types
• Restricted Positive Quantification Is Not Elementary
• How Hard Is Positive Quantification?
• On existential theorems in non-classical functional calculi
• Introduction to Mathematical Logic (PMS-13)
• On the Mints Hierarchy in First-Order Intuitionistic Logic

This page was built for publication: On the Mints Hierarchy in First-Order Intuitionistic Logic