文章基本信息

标题：Automata Theoretic Account of Proof Search
本地全文：下载
作者：Aleksy Schubert ; Wil Dekkers ; Henk P. Barendregt 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：41
页码：128-143
DOI：10.4230/LIPIcs.CSL.2015.128
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：simple types; automata; trees; languages of proofs