2026-07-29T13:40:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5411 2024-03-06T10:36:24Z ddc:004 open_access

Automata Theoretic Account of Proof Search Schubert, Aleksy Dekkers, Wil Barendregt, Henk P. simple types automata trees languages of proofs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Aleksy Schubert and Wil Dekkers and Henk P. Barendregt 2015 Is Part Of LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2015.128 urn:nbn:de:0030-drops-54113 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.128 eng https://creativecommons.org/licenses/by/3.0/legalcode