Loading...
Please wait, while we are loading the content...
Similar Documents
Automata theory approach to predicate intuitionistic logic
| Content Provider | Oxford Academic |
|---|---|
| Author | Zielenkiewicz, Maciej Schubert, Aleksy |
| Copyright Year | 2022 |
| 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. |
| Related Links | https://academic.oup.com/logcom/article-pdf/32/3/554/43365799/exab069.pdf |
| Ending Page | 580 |
| Starting Page | 554 |
| File Format | |
| ISSN | 0955792X |
| e-ISSN | 1465363X |
| DOI | 10.1093/logcom/exab069 |
| Journal | Journal of Logic and Computation |
| Issue Number | 3 |
| Volume Number | 32 |
| Language | English |
| Publisher | Oxford Academic |
| Publisher Date | 2022-04-12 |
| Access Restriction | Open |
| Subject Keyword | Computer Architecture and Logic Design Computer Science Science and Mathematics |
| Content Type | Text |
| Resource Type | Article |
| Subject | Logic Theoretical Computer Science Hardware and Architecture Software |
