Axiomatising the logic of computer programming

zbMath0474.68045MaRDI QIDQ1158956

Robert Goldblatt

Publication date: 1982

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

modal logiclogics of programscorrectness of programswhile programssemantical completenesscanonical model constructionsinfinitary inference rule for reasoning about iteration programsproof theory for programming language semantics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01)

Related Items (39)

A case study in the mechanical verification of fault tolerance ⋮ A model existence theorem in infinitary propositional modal logic ⋮ Hyperboolean Algebras and Hyperboolean Modal Logic ⋮ A dynamic logic of action ⋮ The Countable Henkin Principle ⋮ Logic of transition systems ⋮ Infinitary propositional normal modal logic ⋮ Logics with group announcements and distributed knowledge: completeness and expressive power ⋮ A logical framework for evolving software systems ⋮ Dynamic extensions of arrow logic ⋮ Notes on logics of metric spaces ⋮ Propositional quantification in logics of contingency ⋮ To be announced ⋮ Logics for actor networks: a two-stage constrained-hybridisation approach ⋮ Dynamic modal logic with counting: when reduction axioms work and fail ⋮ Branching versus linear logics yet again ⋮ Semantical analysis of specification logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Determinism and non-determinism in PDL ⋮ Coalition and relativised group announcement logic ⋮ Axiomatizing fixpoint logics ⋮ Getting started: Beginnings in the logic of action ⋮ Action incompleteness ⋮ Local properties in modal logic ⋮ ‘KNOWABLE’ AS ‘KNOWN AFTER AN ANNOUNCEMENT’ ⋮ Group announcement logic ⋮ Monadic bounded algebras ⋮ Strong completeness and limited canonicity for PDL ⋮ Temporal Logics with Reference Pointers and Computation Tree Logics ⋮ Erratum to: ``Strong completeness and limited canonicity for PDL ⋮ Announcement as effort on topological spaces ⋮ PDL with intersection of programs: a complete axiomatization ⋮ Quantifier-free epistemic term-modal logic with assignment operator ⋮ Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs? ⋮ Modal logic with names ⋮ A Hybridization of Irreflexive Modal Logics ⋮ Complete Axiomatization of a Relative Modal Logic with Composition and Intersection ⋮ An essay in combinatory dynamic logic

This page was built for publication: Axiomatising the logic of computer programming