Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2405.15822 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913362348081152 |
|---|---|
| author | Amato, Gianluca DeMarco, Mary Lipton, James |
| author_facet | Amato, Gianluca DeMarco, Mary Lipton, James |
| contents | This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog programming language, and proves soundness and completeness of resolution. The semantics and the proof of completeness of the formal system is shown in several ways, suitably adapted to deal with the impredicativity of higher-order logic, which rules out definitions of truth based on induction on formula structure. First, we use the least fixed point of a certain operator on interpretations, in the style of Apt and Van Emden, Then a constructive completeness theorem is given using a proof theoretic variant of the Lindenbaum algebra, which also contains a new approach to establishing cut-elimination. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_15822 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog Amato, Gianluca DeMarco, Mary Lipton, James Programming Languages Logic in Computer Science Logic 68N17 D.6.1 This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog programming language, and proves soundness and completeness of resolution. The semantics and the proof of completeness of the formal system is shown in several ways, suitably adapted to deal with the impredicativity of higher-order logic, which rules out definitions of truth based on induction on formula structure. First, we use the least fixed point of a certain operator on interpretations, in the style of Apt and Van Emden, Then a constructive completeness theorem is given using a proof theoretic variant of the Lindenbaum algebra, which also contains a new approach to establishing cut-elimination. |
| title | Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog |
| topic | Programming Languages Logic in Computer Science Logic 68N17 D.6.1 |
| url | https://arxiv.org/abs/2405.15822 |