On Strictly Arithmetical Completeness in Logics of Programs
1991 (English)In: Theoretical Computer Science, ISSN 0304-3975, Vol. 79, no 2, 341-355Article in journal (Refereed) Published
We introduce and discuss a notion of strictly arithmetical completeness related to relative completeness of Cook (1978) and arithmetical completeness of Harel (1978). We present a powerful technique of obtaining strictly arithmetical axiomatizations of logics of programs. Given a model-theoretic semantics of a logic and a set of formulae defining (in a metalanguage) its nonclassical connectives, we automatically derive strictly arithmetically complete and sound proof systems for this logic. As examples of application of the technique we obtain new axiomatizations of algorithmic logic, (concurrent) dynamic logic and temporal logic.
National CategoryEngineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-74975DOI: 10.1016/0304-3975(91)90336-ZOAI: oai:DiVA.org:liu-74975DiVA: diva2:499807