Document Open Access Logo

Restricted Positive Quantification Is Not Elementary

Authors Aleksy Schubert, Pawel Urzyczyn, Daria Walukiewicz-Chrzaszcz

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2014.251.pdf
  • Filesize: 0.61 MB
  • 23 pages

Document Identifiers

Author Details

Aleksy Schubert
Pawel Urzyczyn
Daria Walukiewicz-Chrzaszcz

Cite As Get BibTex

Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz. Restricted Positive Quantification Is Not Elementary. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 251-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TYPES.2014.251

Abstract

We show that a restricted variant of constructive predicate logic with positive (covariant) quantification is of super-elementary complexity. The restriction is to limit the number of eigenvariables used in quantifier introductions rules to a reasonably usable level. This construction suggests that the known non-elementary decision algorithms for positive logic may actually be best possible.

Subject Classification

Keywords
  • constructive logic
  • complexity
  • automata theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Ulrich Berger, Kenji Miyamoto, Helmut Schwichtenberg, and Monika Seisenberger. Minlog: a tool for program extraction supporting algebras and coalgebras. In Proc. of CALCO'11, volume 6859 of LNCS, pages 393-399. Springer, 2011. Google Scholar
  2. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  3. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, volume 5674 of LNCS, pages 73-78. Springer, 2009. Google Scholar
  4. Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986. Google Scholar
  5. The Coq Development Team. The Coq Proof Assistant. Reference Manual. INRIA, December 2011. Google Scholar
  6. Gilles Dowek and Ying Jiang. Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Theoretical Computer Science, 360(1-3):193-208, 2006. Google Scholar
  7. Gilles Dowek and Ying Jiang. Enumerating proofs of positive formulae. Computer Journal, 52(7):799-807, 2009. Google Scholar
  8. Georges Gonthier. The four colour theorem: Engineering of a formal proof. In D. Kapur, editor, Computer Mathematics, volume 5081 of LNCS. Springer, 2008. Google Scholar
  9. Georges Gonthier. Advances in the formalization of the odd order theorem. In M. van Eekelen, H. Geuvers, J. Schmaltz, and F. Wiedijk, editors, Interactive Theorem Proving, volume 6898 of LNCS, page 2. Springer, 2011. Google Scholar
  10. Gerwin Klein et al. seL4: Formal verification of an OS kernel. Communications of the ACM, 53(6):107-115, 2010. Google Scholar
  11. Daniel Leivant. Monotonic use of space and computational complexity over abstract structures. Technical Report CMU-CS-89-21, Carnegie Mellon University, 1989. Google Scholar
  12. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009. Google Scholar
  13. Grigori E. Mints. Solvability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers. Steklov Inst., 98:135-145, 1968. Google Scholar
  14. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  15. Jens Otten. ileanTAP: An intuitionistic theorem prover. In D. Galmiche, editor, Proc. of TABLEAUX'97, volume 1227 of LNCS, pages 307-312. Springer, 1997. Google Scholar
  16. Ivar Rummelhoff. Polymorphic Π 1 Types and a Simple Approach to Propositions, Types and Sets. PhD thesis, University of Oslo, 2007. Google Scholar
  17. Aleksy Schubert, Paweł Urzyczyn, and Daria Walukiewicz-Chrząszcz. Positive logic is not elementary. Presentation at the Highlights conference, 2013. Google Scholar
  18. Aleksy Schubert, Paweł Urzyczyn, and Daria Walukiewicz-Chrząszcz. How hard is positive quantification? In preparation, 2014. Google Scholar
  19. Aleksy Schubert, Paweł Urzyczyn, and Konrad Zdanowski. On the Mints hierarchy in first-order intuitionistic logic. In A. Pitts, editor, Foundations of Software Science and Computation Structures 2015, volume 9034 of LNCS, pages 451-465. Springer, 2015. Google Scholar
  20. Morten H. Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. Google Scholar
  21. Hao Wang. A variant to Turing’s theory of computing machines. Journal of the ACM, 4(1):63-92, 1957. Google Scholar
  22. Tao Xue and Qichao Xuan. Proof search and counter model of positive minimal predicate logic. ENTCS, 212(0):87-102, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact