Document Open Access Logo

Automata Theoretic Account of Proof Search

Authors Aleksy Schubert, Wil Dekkers, Henk P. Barendregt

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.128.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Aleksy Schubert
Wil Dekkers
Henk P. Barendregt

Cite As Get BibTex

Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt. Automata Theoretic Account of Proof Search. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 128-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.128

Abstract

Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automata-theoretic model for inhabitant search, which can be viewed as proof search by the Curry-Howard isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata.

Subject Classification

Keywords
  • simple types
  • automata
  • trees
  • languages of proofs

Metrics

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

References

  1. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. Google Scholar
  2. Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard, and Camille Vacher. The emptiness problem for tree automata with global constraints. In Jean-Pierre Jouannaud, editor, Proceedings of the LICS 2010, pages 263-272. IEEE Computer Society, 2010. Google Scholar
  3. Choukri-Bey Ben-Yelles. Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, Mathematics Department, University of Wales, Swansea, UK, 1979. Google Scholar
  4. Sabine Broda and Luís Damas. On long normal inhabitants of a type. Journal of Logic and Computation, 15(3):353-390, 2005. Google Scholar
  5. Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57:795-807, 9 1992. Google Scholar
  6. Boris Düdder, Moritz Martens, and Jakob Rehof. Staged composition synthesis. In Zhong Shao, editor, Proceedings of ESOP 2014, volume 8410 of LNCS, pages 67-86. Springer, 2014. Google Scholar
  7. Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13(3-5):341-363, 2002. Google Scholar
  8. Silvia Ghilezan. Inhabitation in intersection and union type assignment systems. Journal of Logic and Computation, 3(6):671-685, 1993. Google Scholar
  9. J. Roger Hindley. Basic simple type theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, 1996. Google Scholar
  10. Jörg Hudelmaier. An o(n log n)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3(1):63-75, 1993. Google Scholar
  11. Michael Kaminski and Nissim Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329-363, 1994. Google Scholar
  12. Michael Kaminski and Tony Tan. Tree automata over infinite alphabets. In A. Avron, N. Dershowitz, and A. Rabinovich, editors, Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of LNCS, pages 386-423. Springer, 2008. Google Scholar
  13. C.-H. Luke Ong and Nikos Tzevelekos. Functional reachability. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA. IEEE Computer Society, 2009. Google Scholar
  14. Dag Prawitz. Natural Deduction. Almqvist and Wiksell, Sweden, 1965. Google Scholar
  15. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Information and Computation, 239:340-355, 2014. Google Scholar
  16. Richard Statman. Intuitionistic propositional logic is PSPACE-complete. Theoretical Computer Science, 9(1):67-72, 1979. Google Scholar
  17. Colin Stirling. Dependency tree automata. In Luca de Alfaro, editor, Proceedings of FOSSACS 2009, volume 5504 of LNCS, pages 92-106. Springer, 2009. Google Scholar
  18. Masako Takahashi, Yohji Akama, and Sachio Hirokawa. Normal proofs and their grammar. Information and Computation, 125(2):144-153, 1996. Google Scholar
  19. Anne Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge University Press, 1996, 2000. Google Scholar
  20. Paweł Urzyczyn. Inhabitation of low-rank intersection types. In Pierre-Louis Curien, editor, Proceedings of TLCA 2009, volume 5608 of LNCS, pages 356-370. Springer, 2009. Google Scholar
  21. Mordchaj Wajsberg. Untersuchungen über den Aussagenkalkül von A. Heyting. Wiadomości Matematyczne, 46, 1938. English translation: On A. Heyting’s propositional calculus, in Mordchaj Wajsberg, Logical Works (S. J. Surma, editor), Ossolineum, Wrocław, 1977, pages 132-171. 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