On relative completeness of Hoare logics
The work
| Authors | Michal Grabowski |
|---|---|
| Editors | |
| Type | article |
| Year | 1985 |
| Citekey | grabowski1985relative |
Where it appeared
| Published in | Information and Control |
|---|---|
| Volume | 66 |
| Issue | 1 |
| Pages | 29--44 |
Identifiers
| DOI | 10.1016/s0019-9958(85)80010-3 |
|---|
Abstract
In this paper a generalization of a certain theorem of Lipton ("Proc. 18th IEEE Sympos. Found. of Comput. Sci." (1977), pp. 1-6) is presented. Namely, we show that for a wide class of programming languages the following holds: the set of all partial correctness assertions true in an expressive interpretation I is uniformly decidable (in I) in the theory of I iff the halting problem is decidable for finite interpretations. In the effect we show that such limitations as effectiveness or Herbrand-definability of interpretation (they are relevant in the previous proofs) can be removed in the case of partial correctness.
A copy is held
pdf, 701.9 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-14 11:32 UTC |
Filed under
Cite it as
@article{grabowski1985relative,
title = {On relative completeness of Hoare logics},
author = {Michal Grabowski},
year = {1985},
journal = {Information and Control},
volume = {66},
number = {1},
pages = {29--44},
doi = {10.1016/s0019-9958(85)80010-3},
}
This record lives at https://refs.drheap.org/grabowski1985relative/ and will keep doing so.