A foundational characterization of Hoare Logic
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918500671422464 |
|---|---|
| author | Leivant, Daniel |
| author_facet | Leivant, Daniel |
| contents | We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to first-order predicates. This equivalence was claimed twice in the past, both with faulty proofs, and seems to be the first foundational characterization of Hoare Logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_13944 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A foundational characterization of Hoare Logic Leivant, Daniel Logic in Computer Science Logic 03F07, 03F35, 03B30 D.2.4; F.3.1; F.3.2; F.1.1; I.2.4 We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to first-order predicates. This equivalence was claimed twice in the past, both with faulty proofs, and seems to be the first foundational characterization of Hoare Logic. |
| title | A foundational characterization of Hoare Logic |
| topic | Logic in Computer Science Logic 03F07, 03F35, 03B30 D.2.4; F.3.1; F.3.2; F.1.1; I.2.4 |
| url | https://arxiv.org/abs/2605.13944 |