{"id":1370,"date":"2011-04-07T15:49:29","date_gmt":"2011-04-07T15:49:29","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1370"},"modified":"2011-05-21T15:50:11","modified_gmt":"2011-05-21T15:50:11","slug":"dao2011-ejercicios-de-deduccion-natural-proposicional-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao2011-ejercicios-de-deduccion-natural-proposicional-con-isabellehol\/","title":{"rendered":"DAO2011: Ejercicios de deducci\u00f3n natural proposicional con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAO2011\">Demostraci\u00f3n asistida por ordenador<\/a> se han comentado las soluciones de los ejercicios de deducci\u00f3n natural proposicional con Isabelle\/HOL\/Isar.<\/p>\n<p>A continuaci\u00f3n se muestra la teor\u00eda correspondiente a los enunciados de los ejercicios<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Deducci\u00f3n natural proposicional *}\r\n\r\ntheory Tema_3_ej\r\nimports Main \r\nbegin \r\n \r\nsection {* Deducci\u00f3n natural proposicional *}\r\n \r\ntext {* Los ejercicios de esta relaci\u00f3n deben de resolverse usando s\u00f3lo\r\n  las reglas b\u00e1sicas de la deducci\u00f3n natural proposicional: \r\n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\r\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\r\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \r\n  \u00b7 notnotD:    \u00ac\u00ac P \u27f9 P\r\n  . notnotI:    P \u27f9 \u00ac\u00ac P\r\n  \u00b7 mp:         \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \r\n  \u00b7 mt:         \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \r\n  \u00b7 impI:       (P \u27f9 Q) \u27f9 P \u27f6 Q\r\n  \u00b7 disjI1:     P \u27f9 P \u2228 Q\r\n  \u00b7 disjI2:     Q \u27f9 P \u2228 Q\r\n  \u00b7 disjE:      \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \r\n  \u00b7 FalseE:     False \u27f9 P\r\n  \u00b7 notE:       \u27e6\u00acP; P\u27e7 \u27f9 R\r\n  \u00b7 notI:       (P \u27f9 False) \u27f9 \u00acP\r\n  \u00b7 iffI:       \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P = Q\r\n  \u00b7 iffD1:      \u27e6Q = P; Q\u27e7 \u27f9 P \r\n  \u00b7 iffD2:      \u27e6P = Q; Q\u27e7 \u27f9 P\r\n  \u00b7 ccontr:     (\u00acP \u27f9 False) \u27f9 P\r\n*}\r\n \r\nlemma notnotI: \"P \u27f9 \u00ac\u00ac P\"\r\nby auto\r\n \r\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\r\nby auto\r\n \r\nlemma ejercicio_1:\r\n  assumes 1: \"p \u27f6 q\" and\r\n          2: \"p\"\r\n  shows \"q\"  \r\noops\r\n \r\nlemma ejercicio_1b:\r\n  assumes 1: \"p \u27f6 q\" and\r\n          2: \"p\"\r\n  shows \"q\"  \r\noops\r\n \r\nlemma ejercicio_2:\r\n  assumes 1: \"p\u27f6q\" and \r\n          2: \"q\u27f6r\" and \r\n          3: \"p\" \r\n  shows \"r\"\r\noops\r\n \r\nlemma ejercicio_3:\r\n  assumes 1: \"p\u27f6(q\u27f6r)\" and \r\n          2: \"p\u27f6q\" and  \r\n          3: \"p\"\r\n  shows \"r\"\r\noops\r\n \r\nlemma ejercicio_4:\r\n  assumes 1: \"p\u27f6q\" and \r\n          2: \"q\u27f6r\" \r\n  shows \"p\u27f6r\"\r\noops\r\n \r\nlemma ejercicio_5:\r\n  assumes 1: \"p\u27f6(q\u27f6r)\"\r\n  shows \"q\u27f6(p\u27f6r)\"\r\noops\r\n \r\nlemma ejercicio_6:\r\n  assumes 1: \"p\u27f6(q\u27f6r)\" \r\n  shows \"(p\u27f6q)\u27f6(p\u27f6r)\"\r\noops\r\n \r\nlemma ejercicio_7:\r\n  assumes 1: \"p\" \r\n  shows \"q\u27f6p\"\r\noops\r\n \r\nlemma ejercicio_8:\r\n  \"p\u27f6(q\u27f6p)\"\r\noops\r\n \r\nlemma ejercicio_9:\r\n  assumes 1: \"p\u27f6q\"  \r\n  shows \"(q\u27f6r)\u27f6(p\u27f6r)\"\r\noops\r\n \r\nlemma ejercicio_10:\r\n  assumes 1: \"p\u27f6(q\u27f6(r\u27f6s))\"\r\n  shows \"r\u27f6(q\u27f6(p\u27f6s))\"\r\noops\r\n \r\nlemma ejercicio_11:\r\n  \"(p\u27f6(q\u27f6r))\u27f6((p\u27f6q)\u27f6(p\u27f6r))\"\r\noops\r\n \r\nlemma ejercicio_12:\r\n  assumes 1: \"(p\u27f6q)\u27f6r\" \r\n  shows \"p\u27f6(q\u27f6r)\"\r\noops\r\n \r\nlemma ejercicio_13:\r\n  assumes 1: \"p\" and  \r\n          2: \"q\" \r\n  shows \"p\u2227q\"\r\noops\r\n \r\nlemma ejercicio_14:\r\n  assumes 1: \"p\u2227q\" \r\n  shows \"p\"\r\noops\r\n \r\nlemma ejercicio_15:\r\n  assumes 1: \"p\u2227q\" \r\n  shows \"q\"\r\noops\r\n \r\nlemma ejercicio_16:\r\n  assumes 1: \"p\u2227(q\u2227r)\"\r\n  shows \"(p\u2227q)\u2227r\"\r\noops\r\n \r\nlemma ejercicio_17:\r\n  assumes 1: \"(p\u2227q)\u2227r\"\r\n  shows \"p\u2227(q\u2227r)\"\r\noops\r\n \r\nlemma ejercicio_18:\r\n  assumes 1: \"p\u2227q\"\r\n  shows \"p\u27f6q\"\r\noops\r\n \r\nlemma ejercicio_19:\r\n  assumes 1: \"(p\u27f6q)\u2227(p\u27f6r)\" \r\n  shows \"p\u27f6q\u2227r\"\r\noops\r\n \r\nlemma ejercicio_20:\r\n  assumes 1: \"p\u27f6q\u2227r\" \r\n  shows \"(p\u27f6q)\u2227(p\u27f6r)\"\r\noops\r\n \r\nlemma ejercicio_21:\r\n  assumes 1: \"p\u27f6(q\u27f6r)\" \r\n  shows \"p\u2227q\u27f6r\"\r\noops\r\n \r\nlemma ejercicio_22:\r\n  assumes 1: \"p\u2227q\u27f6r\"  \r\n  shows \"p\u27f6(q\u27f6r)\"\r\noops\r\n \r\nlemma ejercicio_23:\r\n  assumes 1: \"(p\u27f6q)\u27f6r\" \r\n  shows \"p\u2227q\u27f6r\"\r\noops\r\n \r\nlemma ejercicio_24:\r\n  assumes 1: \"p\u2227(q\u27f6r)\"  \r\n  shows \"(p\u27f6q)\u27f6r\"\r\noops\r\n \r\nlemma ejercicio_25:\r\n  assumes 1: \"p\" \r\n  shows \"p\u2228q\"\r\noops\r\n \r\nlemma ejercicio_26:\r\n  assumes 1: \"q\"  \r\n  shows \"p\u2228q\"\r\noops\r\n \r\nlemma ejercicio_27:\r\n  assumes 1: \"p\u2228q\" \r\n  shows \"q\u2228p\"\r\noops\r\n \r\nlemma ejercicio_28:\r\n  assumes 1: \"q\u27f6r\" \r\n  shows \"p\u2228q\u27f6p\u2228r\"\r\noops\r\n \r\nlemma ejercicio_29:\r\n  assumes 1: \"p\u2228p\" \r\n  shows \"p\"\r\noops\r\n \r\nlemma ejercicio_30:\r\n  assumes 1: \"p\" \r\n  shows \"p\u2228p\"\r\noops\r\n \r\nlemma ejercicio_31:\r\n  assumes 1: \"p\u2228(q\u2228r)\"\r\n  shows \"(p\u2228q)\u2228r\"\r\noops\r\n \r\nlemma ejercicio_32:\r\n  assumes 1: \"(p\u2228q)\u2228r\"\r\n  shows \"p\u2228(q\u2228r)\"\r\noops\r\n \r\nlemma ejercicio_33:\r\n  assumes 1: \"p\u2227(q\u2228r)\" \r\n  shows \"(p\u2227q)\u2228(p\u2227r)\"\r\noops\r\n \r\nlemma ejercicio_34:\r\n  assumes 1: \"(p\u2227q)\u2228(p\u2227r)\" \r\n  shows \"p\u2227(q\u2228r)\"\r\noops\r\n \r\nlemma ejercicio_35:\r\n  assumes 1: \"p\u2228(q\u2227r)\"\r\n  shows \"(p\u2228q)\u2227(p\u2228r)\"\r\noops\r\n \r\nlemma ejercicio_36:\r\n  assumes 1: \"(p\u2228q)\u2227(p\u2228r)\"\r\n  shows \"p\u2228(q\u2227r)\"\r\noops\r\n \r\nlemma ejercicio_37:\r\n  assumes 1: \"(p\u27f6r)\u2227(q\u27f6r)\" \r\n  shows \"p\u2228q\u27f6r\"\r\noops\r\n \r\nlemma ejercicio_38:\r\n  assumes 1: \"p\u2228q\u27f6r\"  \r\n  shows \"(p\u27f6r)\u2227(q\u27f6r)\"\r\noops\r\n \r\nlemma ejercicio_39:\r\n  assumes 1: \"p\"\r\n  shows \"\u00ac\u00acp\"\r\noops\r\n \r\nlemma ejercicio_40:\r\n  assumes 1: \"\u00acp\"  \r\n  shows \"p\u27f6q\"\r\noops\r\n \r\nlemma ejercicio_41:\r\n  assumes 1: \"p\u27f6q\"\r\n  shows \"\u00acq\u27f6\u00acp\"\r\noops\r\n \r\nlemma ejercicio_42:\r\n  assumes 1: \"p\u2228q\" and\r\n          2: \"\u00acq\" \r\n  shows \"p\"\r\noops\r\n \r\nlemma ejercicio_43:\r\n  assumes 1: \"p\u2228q\" and\r\n          2: \"\u00acp\" \r\n  shows \"q\"\r\noops\r\n \r\nlemma ejercicio_44:\r\n  assumes 1: \"p\u2228q\"\r\n  shows \"\u00ac(\u00acp\u2227\u00acq)\"\r\noops\r\n \r\nlemma ejercicio_45:\r\n  assumes 1: \"p\u2227q\"\r\n  shows \"\u00ac(\u00acp\u2228\u00acq)\"\r\noops\r\n \r\nlemma ejercicio_46:\r\n  assumes 1: \"\u00ac(p\u2228q)\"\r\n  shows \"\u00acp\u2227\u00acq\"\r\noops\r\n \r\nlemma ejercicio_47:\r\n  assumes 1: \"\u00acp\u2227\u00acq\"  \r\n  shows \"\u00ac(p\u2228q)\"\r\noops\r\n \r\nlemma ejercicio_48:\r\n  assumes 1: \"\u00acp\u2228\u00acq\"\r\n  shows \"\u00ac(p\u2227q)\"\r\noops\r\n \r\nlemma ejercicio_49:\r\n  \"\u00ac(p\u2227\u00acp)\"\r\noops\r\n \r\nlemma ejercicio_50:\r\n  assumes 1: \"p\u2227\u00acp\"\r\n  shows \"q\"\r\noops\r\n \r\nlemma ejercicio_51:\r\n  assumes 1: \"\u00ac\u00acp\"\r\n  shows \"p\"\r\noops\r\n \r\nlemma ejercicio_52:\r\n  \"p\u2228\u00acp\"\r\noops\r\n \r\nlemma ejercicio_53:\r\n  \"((p\u27f6q)\u27f6p)\u27f6p\"\r\noops\r\n \r\nlemma ejercicio_54:\r\n  assumes 1: \"\u00acq\u27f6\u00acp\"\r\n  shows \"p\u27f6q\"\r\noops\r\n \r\nlemma ejercicio_55:\r\n  assumes 1: \"\u00ac(\u00acp\u2227\u00acq)\"\r\n  shows \"p\u2228q\"\r\noops\r\n \r\nlemma ejercicio_56:\r\n  assumes 1: \"\u00ac(\u00acp\u2228\u00acq)\"\r\n  shows \"p\u2227q\"\r\noops\r\n \r\nlemma ejercicio_57:\r\n  assumes 1: \"\u00ac(p\u2227q)\"\r\n  shows \"\u00acp\u2228\u00acq\"\r\noops\r\n \r\nlemma ejercicio_58:\r\n  \"(p\u27f6q)\u2228(q\u27f6p)\"\r\noops\r\n \r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Demostraci\u00f3n asistida por ordenador se han comentado las soluciones de los ejercicios de deducci\u00f3n natural proposicional con Isabelle\/HOL\/Isar. A continuaci\u00f3n se muestra la teor\u00eda correspondiente a los enunciados de los ejercicios<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[165],"tags":[289],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1370"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=1370"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1370\/revisions"}],"predecessor-version":[{"id":1371,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1370\/revisions\/1371"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1370"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1370"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1370"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}