Paper Info
Title
Automata theory approach to predicate intuitionistic logic
Abstract
Predicate intuitionistic logic is a well-established fragment of dependent types. Proof construction in this logic, as the Curry-Howard isomorphism states, is the process of program synthesis. We present automata that can handle proof construction and program synthesis in full intuitionistic first-order logic. Given a formula, we can construct an automaton such that the formula is provable if and only if the automaton has an accepting run. As further research, this construction makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections with the traditional logical connectives.
Year
DOI
Venue
2022
10.1093/logcom/exab069
JOURNAL OF LOGIC AND COMPUTATION
Keywords
DocType
Volume
First-order logic, automata theory, Curry-Howard isomorphism, proof search, program synthesis
Journal
32
Issue
ISSN
Citations 
3
0955-792X
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Maciej Zielenkiewicz100.34
Aleksy Schubert28017.99