LiU Electronic Press
Full-text not available in DiVA
Author:
Szalas, Andrzej (University of Warsaw)
Title:
On Strictly Arithmetical Completeness in Logics of Programs
Publication type:
Article in journal (Refereed)
Language:
English
Publisher: Elsevier
Status:
Published
In:
Theoretical Computer Science(ISSN 0304-3975)
Volume:
79
Issue:
2
Pages:
341-355
Year of publ.:
1991
URI:
urn:nbn:se:liu:diva-74975
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-74975
Subject category:
Engineering and Technology
Abstract(en) :

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.

Available from:
2012-02-13
Created:
2012-02-13
Last updated:
2012-02-22
Statistics:
9 hits