21st Annual IEEE Symposium on Logic in Computer Science (LICS'06) Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic Seattle, Washington August 12-August 15 ISBN: 0-7695-2631-4
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.33
We establish a match between two broad approaches to reasoning about programs: modal (dynamic logic) proofs on the one hand, and explicit higher-order reference to program semantics, on the other. We show that Pratt-Segerberg?s firstorder dynamic logic DL proves precisely program properties that are provable in second-order logic with set-existence restricted to a natural class of formulas, well-known to be related to computation theory
Citation:
Daniel Leivant, "Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic," lics, pp.157-168, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb