loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Daniel Leivant, Indiana University, USA
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.