A Natural Deduction Approach to Dynamic Logic

@article{citeulike:1926823, abstract = {. Natural Deduction style presentations of program logics are useful in view of the implementation of such logics in interactive proof development environments, based on type theory, such as LEGO, Coq, etc. In fact, ND-style systems are the kind of systems which can take best advantage of the possibility of reasoning \"under assumptions\" offered by proof assistants generated by Logical Frameworks. In this paper we introduce and discuss sound and complete proof systems in Natural Deduction style...}, author = {Honsell, F. and Miculan, M. }, citeulike-article-id = {1926823}, journal = {Lecture Notes in Computer Science}, keywords = {dynamic\_logic}, pages = {165--??}, posted-at = {2007-11-16 15:48:13}, priority = {2}, title = {A Natural Deduction Approach to Dynamic Logic}, url = {http://citeseer.ist.psu.edu/54767.html}, volume = {1158}, year = {1996} }

TY - JOUR ID - citeulike:1926823 L3 - citeulike-article-id:1926823 TI - A Natural Deduction Approach to Dynamic Logic JF - Lecture Notes in Computer Science VL - 1158 SP - 165 EP - ?? N2 - . Natural Deduction style presentations of program logics are useful in view of the implementation of such logics in interactive proof development environments, based on type theory, such as LEGO, Coq, etc. In fact, ND-style systems are the kind of systems which can take best advantage of the possibility of reasoning "under assumptions" offered by proof assistants generated by Logical Frameworks. In this paper we introduce and discuss sound and complete proof systems in Natural Deduction style... KW - dynamic_logic AU - Honsell, F AU - Miculan, M PY - 1996/// UR - http://citeseer.ist.psu.edu/54767.html ER -