{"id":287,"date":"2010-07-30T09:54:00","date_gmt":"2010-07-30T09:54:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/reanudacion\/"},"modified":"2013-03-08T05:53:43","modified_gmt":"2013-03-08T05:53:43","slug":"reanudacion","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/reanudacion\/","title":{"rendered":"Reanudaci\u00f3n"},"content":{"rendered":"<p>Despu\u00e9s de 4 meses, reanudo la escritura en Vestigium. Como uno de sus objetivos era servir de diario de las publicaciones en <a href=\"http:\/\/www.cs.us.es\/~jalonso\">mi sitio en la Red<\/a>, voy a resumir las realizadas desde la anterior entrada en Vestigium.<\/p>\n<p>He publicado una introducci\u00f3n al sistema de c\u00e1lculo simb\u00f3lico <a href=\"http:\/\/maxima.sourceforge.net\/es\">Maxima<\/a> que he usado en las asignaturas de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\">I1M (Inform\u00e1tica de 1\u00ba de Matem\u00e1ticas)<\/a> como en la de <a href=\"https:\/\/www.glc.us.es\/~jalonso\/SLEAM2010\/index.php5\/Software_Libre_para_la_Ense%C3%B1anza_y_el_Aprendizaje_de_las_Matem%C3%A1ticas\">SLEAM (Sofware libre para la ense\u00f1anza y aprendizaje de las Matem\u00e1ticas)<\/a>. Los temas y ejercicios publicados son los siguientes:<\/p>\n<ul>\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-14.html\"> Tema 14: Introducci\u00f3n a Maxima<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-15.html\"> Tema 15: Funciones de una variable<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-16.html\"> Tema 16: Aritm\u00e9tica<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-17.html\"> Tema 17: Sucesiones y recursi\u00f3n<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-18.html\"> Tema 18: Programaci\u00f3n<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-19.html\"> Tema 19: Matrices en Maxima<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-20.html\"> Tema 20: Gr\u00e1ficos y animaciones<\/a>.<\/ul>\n<p>las relaciones de ejercicios:<\/p>\n<ul>\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/ejercicios\/G1_Rel_24.html\"> Relaci\u00f3n 24<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/ejercicios\/G1_Rel_25\/G1_Rel_25.html\"> Relaci\u00f3n 25<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/ejercicios\/G1_Rel_26\/G1_Rel_26.html\"> Relaci\u00f3n 26<\/a>.<\/ul>\n<p>Adem\u00e1s, en <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\"> I1M (Inform\u00e1tica de 1\u00ba de Matem\u00e1ticas)<\/a> he publicado dos nuevos temas sobre dise\u00f1o de algoritmos con Haskell:<\/p>\n<ul>\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/temas\/tema-21.pdf\"> Tema 21: Algoritmos de exploraci\u00f3n de grafos<\/a>.\n<li> <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/tema-22.html\"> Tema 22: Tipos de datos: Polinomios<\/a>.<\/ul>\n<p>En la p\u00e1gina de publicaciones he a\u00f1adido las dos m\u00e1s recientes:<\/p>\n<ul>\n<li> <a href=\"http:\/\/dx.doi.org\/10.1016\/j.matcom.2010.05.024\"> A logic approach to decision taking in a railway interlocking system using Maple<\/a>.  Mathematics and Computers in Simulation (En colaboraci\u00f3n con E. Roanes, A. Hernando y L.M. Laita).\n<li> <a href=\"http:\/\/bit.ly\/c2oWsz\"> Proof Pearl: a Formal Proof of Higman&#8217;s Lemma in ACL2<\/a>. Journal of Automated Reasoning. (En colaboraci\u00f3n con F.J. Mart\u00edn, J.L. Ruiz y M.J. Hidalgo).<\/ul>\n<p>Finalmente, en la <a href=\"https:\/\/www.glc.us.es\/wiki\/Computational_Logic_Group\">wiki del Grupo de L\u00f3gica Computacional<\/a> he a\u00f1adido las formalizaciones de teor\u00edas en <a href=\"http:\/\/pvs.csl.sri.com\/\"> PVS<\/a>:<\/p>\n<ul>\n<li> <a href=\"https:\/\/www.glc.us.es\/wiki\/A_Formalization_of_Abstract_Properties_of_Confluent_Reductions_in_PVS\"> A Formalization of Abstract Properties of Confluent Reductions in PVS<\/a>.\n<li> <a href=\"https:\/\/www.glc.us.es\/wiki\/Proving_termination_with_multiset_orderings_in_PVS:_theory%2C_methodology_and_applications_%28PROTEMO%29\"> Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)<\/a>.\n<li> <a href=\"https:\/\/www.glc.us.es\/wiki\/A_formally_verified_prover_for_the_ALC_description_logic_%28in_PVS%29\"> A formally verified prover for the ALC description logic (in PVS)<\/a>.\n<li> <a href=\"https:\/\/www.glc.us.es\/wiki\/Verification_of_the_formal_concept_analysis_in_PVS\"> Verification of the formal concept analysis in PVS<\/a>.\n<li> <a href=\"https:\/\/www.glc.us.es\/wiki\/A_formally_verified_proof_in_PVS_of_the_strong_completeness_theorem_of_propositional_SLD-resolution\"> A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution<\/a>.\n<li> <a href=\"https:\/\/www.glc.us.es\/wiki\/Theory_of_Refinements_in_PVS\"> Theory of Refinements in PVS<\/a>.<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Despu\u00e9s de 4 meses, reanudo la escritura en Vestigium. Como uno de sus objetivos era servir de diario de las publicaciones en mi sitio en la Red, voy a resumir las realizadas desde la anterior entrada en Vestigium. He publicado una introducci\u00f3n al sistema de c\u00e1lculo simb\u00f3lico Maxima que he usado en las asignaturas de&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","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":[7],"tags":[75,279,281,277,273,78,272],"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\/287"}],"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=287"}],"version-history":[{"count":10,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/287\/revisions"}],"predecessor-version":[{"id":3052,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/287\/revisions\/3052"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=287"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=287"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=287"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}