How hard is positive quantification?

DOI10.1145/2981544MaRDI QIDQ5278190zbMATH OpenOpenAlexFDO

Authors Aleksy Schubert, Paweł Urzyczyn, Daria Walukiewicz-Chrząszcz

Publication date 13 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2981544

zbMATH Keywords

automatacomplexityintuitionistic logicpositive quantification

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Automata and formal grammars in connection with logical questions (03D05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Restricted positive quantification is not elementary
• Proof Search and Counter Model of Positive Minimal Predicate Logic
• On the complexity of propositional quantification in intuitionistic logic
• First-order linear logic without modalities is NEXPTIME-hard
• Eigenvariables, bracketing and the decidability of positive minimal predicate logic

Cites work

• A Brief Overview of Agda – A Functional Language with Dependent Types
• Advances in the Formalization of the Odd Order Theorem
• Descriptive characterizations of computational complexity
• Eigenvariables, bracketing and the decidability of positive minimal predicate logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Lectures on the Curry-Howard isomorphism
• On the Mints hierarchy in first-order intuitionistic logic
• Proof Search and Counter Model of Positive Minimal Predicate Logic
• Sovability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers
• The Four Colour Theorem: Engineering of a Formal Proof
• Theory of computation.
• Translations on a context free grammar

Cited in

(3)

• Restricted positive quantification is not elementary
• On the Mints hierarchy in first-order intuitionistic logic
• Duality in intuitionistic propositional logic

Describes a project that uses

Uses Software

• Agda
• Coq
• Isabelle/HOL
• Nuprl
• seL4

This page was built for publication: How hard is positive quantification?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5278190)