LCS Publication Details
Publication Title: ARITHMETICAL COMPLETENESS IN LOGICS OF PROGRAMS
Publication Author: Harel, David
Additional Authors:
LCS Document Number: MIT-LCS-TM-103
Publication Date: 4-1-1978
LCS Group: No Group Specified
Additional URL: No URL Given
Abstract:
We consider the problem of designing arithmetically complete axiom systems for proving general properties programs ; i.e.axiom systems which are complete over arithmetical universes, when all first-order formulae which are valid in such universes are taken as axioms. We prove a general Theorem of Completeness which takes care of a major part of the responsibility when designing such systems. It is then shown that what is left to do in order to establish an arithmetical completeness result, such as those appearing in [12] and [14] for the logics DL and DL+, can be described as a chain of reasoning which involves some simple utilizations of arithmetical induction. An immediate application of these observations is given in the form of arithmetical completeness result for a new logic similar to that of Salwicki [22]. Finally, we contrast this discipline with Cook's [5] notion of relative completeness.
To obtain this publication:

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