Hoare's Logic Is Not Complete When It Could Be
| dc.contributor.author | Bergstra, J. | en_US |
| dc.contributor.author | Chielinksa, A. | en_US |
| dc.contributor.author | Tiuryn, J. | en_US |
| dc.date.accessioned | 2023-03-29T14:21:45Z | |
| dc.date.available | 2023-03-29T14:21:45Z | |
| dc.date.issued | 1982-08 | |
| dc.identifier.uri | https://hdl.handle.net/1721.1/149036 | |
| dc.description.abstract | It is known (cf.[2]) that is the Hoare rules are complete for a first-order structure A, then the set of partial correctness assertions true over A is recursive in the first-order theory of A. We show that the converse is not true. Namely, there is a first-order structure C such that the set of partial correctness assertions true over C is recursive in the theory of C, but the Hoare rules are not complete for C. | en_US |
| dc.relation.ispartofseries | MIT-LCS-TM-226 | |
| dc.title | Hoare's Logic Is Not Complete When It Could Be | en_US |
| dc.identifier.oclc | 10741982 |
