Studia Logica 47 (3):279 - 301 (1988)

The main result of this paper belongs to the field of the comparative study of program verification methods as well as to the field called nonstandard logics of programs. We compare the program verifying powers of various well-known temporal logics of programs, one of which is the Intermittent Assertions Method, denoted as Bur. Bur is based on one of the simplest modal logics called S5 or sometime-logic. We will see that the minor change in this background modal logic increases the program verifying power of Bur. The change can be described either technically as replacing the reflexive version of S5 with an irreflexive version, or intuitively as using the modality some-other-time instead of sometime. Some insights into the nature of computational induction and its variants are also obtained.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/BF00370557
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 55,935
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Completeness in the Theory of Types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.

Add more references

Citations of this work BETA

Derivation Rules as Anti-Axioms in Modal Logic.Yde Venema - 1993 - Journal of Symbolic Logic 58 (3):1003-1034.
Taming Logic.Maarten Marx, Szabolcs Mikul & István Németi - 1995 - Journal of Logic, Language and Information 4 (3):207-226.

Add more citations

Similar books and articles


Added to PP index

Total views
18 ( #558,208 of 2,403,023 )

Recent downloads (6 months)
1 ( #552,435 of 2,403,023 )

How can I increase my downloads?


My notes