The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
A new incompleteness result for Hoare's system
The work
| Authors | Mitchell Wand |
|---|---|
| Editors | |
| Type | misc |
| Year | 1976 |
| Citekey | wand1976incompleteness |
Where it appeared
| Published in | ACM Symposium on Theory of Computing (STOC) |
|---|---|
| Pages | 87--91 |
Identifiers
| DOI | 10.1145/800113.803635 |
|---|---|
| OpenAlex | W2129865151 |
Access
| Landing page | https://doi.org/10.1145/800113.803635 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/800113.803635 |
Related
| Superseded by | wand1978incompleteness |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
A structure A is presented for which Hoare's formal system for partial correctness is incomplete, even if the entire first-order theory of A is included among the axioms. It follows that the language of first-order logic is insufficient to express all loop invariants. The implications of this result for program-proving are discussed.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 06:33 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@misc{wand1976incompleteness,
title = {A new incompleteness result for Hoare's system},
author = {Mitchell Wand},
year = {1976},
journal = {ACM Symposium on Theory of Computing (STOC)},
pages = {87--91},
doi = {10.1145/800113.803635},
}
This record lives at https://refs.drheap.org/wand1976incompleteness/ and will keep doing so.