David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
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)|
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
Leon Henkin (1950). Completeness in the Theory of Types. Journal of Symbolic Logic 15 (2):81-91.
Leon Henkin (1950). Review: Laszlo Kalmar, Une Forme du Theoreme de Godel Sous des Hypotheses Minimales; Laszlo Kalmar, Quelques Formes Generales du Theoreme de Godel. [REVIEW] Journal of Symbolic Logic 15 (3):230-230.
Citations of this work BETA
Maarten Marx, Szabolcs Mikul & István Németi (1995). Taming Logic. Journal of Logic, Language and Information 4 (3):207-226.
Balázs Biró & Ildikó Sain (1993). Peano Arithmetic as Axiomatization of the Time Frame in Logics of Programs and in Dynamic Logics. Annals of Pure and Applied Logic 63 (3):201-225.
Similar books and articles
Anita Wasilewska (1985). Programs and Logics. Studia Logica 44 (2):125 - 137.
Carlos Viegas Damásio & Luís Moniz Pereira (2002). Hybrid Probabilistic Logic Programs as Residuated Logic Programs. Studia Logica 72 (1):113 - 138.
Ganesh Baliga, John Case, Sanjay Jain & Mandayam Suraj (1994). Machine Learning of Higher-Order Programs. Journal of Symbolic Logic 59 (2):486-500.
Timothy R. Colburn (1991). Program Verification, Defeasible Reasoning, and Two Views of Computer Science. Minds and Machines 1 (1):97-116.
Francis J. Pelletier (1993). Identity in Modal Logic Theorem Proving. Studia Logica 52 (2):291 - 308.
Reinhard Muskens (1999). On Partial and Paraconsistent Logics. Notre Dame Journal of Formal Logic 40 (3):352-374.
David A. Nelson (1992). Deductive Program Verification (a Practitioner's Commentary). Minds and Machines 2 (3):283-307.
Aleksandar Ignjatović (1994). Hilbert's Program and the Omega-Rule. Journal of Symbolic Logic 59 (1):322-343.
Added to index2009-01-28
Total downloads6 ( #336,406 of 1,726,085 )
Recent downloads (6 months)2 ( #289,836 of 1,726,085 )
How can I increase my downloads?