LCS Publication Details
Publication Title: "HOARE'S LOGIC IS NOT COMPLETE WHEN IT COULD BE"
Publication Author: Bergstra, J.
Additional Authors: Chmielinska, A. and Tiuryn, J.
LCS Document Number: MIT-LCS-TM-226
Publication Date: 8-1-1982
LCS Group: No Group Specified
Additional URL: No URL Given
Abstract:
It is known (cf.[2]) that if the Hoare rules are complete for a first-order structure A, then the set of partial correctness assertions true over A is resursive 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 resursive in the theory of C, but the Hoare rules are not complete for C.
To obtain this publication:

    To purchase a printed copy of this publication please contact MIT Document Services.