{"id":7182,"date":"2020-05-17T10:22:41","date_gmt":"2020-05-17T08:22:41","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7182"},"modified":"2020-05-17T10:23:08","modified_gmt":"2020-05-17T08:23:08","slug":"videos-de-las-clases-de-razonamiento-automatico-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/videos-de-las-clases-de-razonamiento-automatico-con-isabelle-hol\/","title":{"rendered":"V\u00eddeos de las clases de razonamiento autom\u00e1tico con Isabelle\/HOL"},"content":{"rendered":"<div id=\"content\">\n<p class=\"title\">Con motivo de la pandemia henos tenido que pasar la docencia al formato no presencial.<\/p>\n<p>En la asignatura de <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf\/\">L\u00f3gica de 3\u00ba de Matem\u00e1tica<\/a> el cambio ha tenido lugar al principio de la segunda parte del curso en la que se estudia el razonamiento autom\u00e1tico con Isabelle\/HOL.<\/p>\n<p>Todas las clases no presenciales las he dado por videoconferencia y he subido sus v\u00eddeos a <a href=\"https:\/\/www.youtube.com\/playlist?list=PLPIlzBVlfbbFZOY6tpFiXMSw0j21OfHVY\">YouTube<\/a>. En este momento hay 12 v\u00eddeos correspondientes a las clases no presenciales impartidas:<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/youtu.be\/vIr0HF5tMRs\">Deducci\u00f3n natural proposicional con Isabelle\/HOL<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/DZjjvM1-DZk\">Deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL (Parte 1 de 2)<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/Hf4uNUHRDfg\">Deducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/HOL (Parte 2 de 2)<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/xu8x0hC_NE4\">Programaci\u00f3n funcional en Isabelle\/HOL<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/1SsdIYcCrmA\">Razonamiento sobre programas con Isabelle\/HOL (Parte 1 de 5)<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/L6neWUbAUso\">Razonamiento sobre programas con Isabelle\/HOL (Parte 2 de 5)<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/lk-UsIOtClk\">Razonamiento sobre programas con Isabelle\/HOL (Parte 3 de 5)<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/R6_MV8r4KFw\">Razonamiento sobre programas con Isabelle\/HOL (Parte 4 de 5)<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/Ai8RC6nbCKo\">Razonamiento sobre programas con Isabelle\/HOL (Parte 5 de 5)<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/si_DTm4ImEM\">Razonamiento por casos y por inducci\u00f3n en Isabelle\/HOL<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/0ZiCWOIgMMc\">Razonamiento sobre \u00e1rboles binarios con Isabelle\/HOL<\/a>.<\/li>\n<li><a href=\"https:\/\/youtu.be\/uytQp1w2Y8I\">\u00c1rboles y bosques: Recursi\u00f3n mutua e inducci\u00f3n con Isabelle\/HOL<\/a>.<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Con motivo de la pandemia henos tenido que pasar la docencia al formato no presencial. En la asignatura de L\u00f3gica de 3\u00ba de Matem\u00e1tica el cambio ha tenido lugar al principio de la segunda parte del curso en la que se estudia el razonamiento autom\u00e1tico con Isabelle\/HOL. Todas las clases no presenciales las he dado&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[334],"tags":[],"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\/7182"}],"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=7182"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7182\/revisions"}],"predecessor-version":[{"id":7184,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7182\/revisions\/7184"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7182"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7182"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7182"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}