{"id":708,"date":"2010-10-08T06:56:54","date_gmt":"2010-10-08T06:56:54","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=708"},"modified":"2013-03-08T05:50:12","modified_gmt":"2013-03-08T05:50:12","slug":"formalizaciones-en-pvs-y-el-problema-de-las-versiones","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formalizaciones-en-pvs-y-el-problema-de-las-versiones\/","title":{"rendered":"Formalizaciones en PVS y el problema de las versiones"},"content":{"rendered":"<p>En la <a href=\"https:\/\/www.glc.us.es\/wiki\/Computational_Logic_Group\">wiki del Grupo de L\u00f3gica Computacional<\/a> se han publicados las formalizaciones en PVS 4.2 de las siguientes teor\u00edas:<\/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>.\n<\/ul>\n<p>\nLa adaptaci\u00f3n la ha realizado <a href=\"http:\/\/www.cs.us.es\/~mjoseh\/\">Mar\u00eda J. Hidalgo<\/a> a partir de la versi\u00f3n de PVS 3.2. El proceso de adaptaci\u00f3n ha sido complejo por las diferencias existentes entre ambas versiones de PVS. Los principales problemas que han aparecido son los siguientes:<\/p>\n<ul>\n<li>Diferencia en el tratamiento de los juicios entre teor\u00edas situadas en distintos directorios y cargadas como extensiones del preludio.\n<li>Diferencia en las opciones por defecto en estrategias predefinidas.\n<li>Diferencia en el n\u00famero de obligaciones de pruebas generadas.\n<\/ul>\n<p>Adem\u00e1s, el problema de la compatibilidad entre las distintas versiones de los sistemas de razonamiento dificulta la reutilizaci\u00f3n de las teor\u00eda formalizadas. En concreto, en algunas teor\u00edas que hemos desarrollado se han usado teor\u00edas desarrolladas por otros como, por ejemplo, la <a href=\"http:\/\/www.informatik.uni-ulm.de\/ki\/PVS\/fixpoints.html\">teor\u00eda sobre puntos fijos<\/a> de F. Bartels, A. Dold, F.W. v. Henke, H. Pfeifer y H. Rue\u00df que est\u00e1 desarrollada en la versi\u00f3n 2.4 de PVS, no se ha adaptado a las siguientes versiones y no es adecuada para la versi\u00f3n actual de PVS.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la wiki del Grupo de L\u00f3gica Computacional se han publicados las formalizaciones en PVS 4.2 de las siguientes teor\u00edas: A Formalization of Abstract Properties of Confluent Reductions in PVS. Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO). A formally verified prover for the ALC description logic (in PVS). Verification of&#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":[21,8],"tags":[89,277],"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\/708"}],"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=708"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/708\/revisions"}],"predecessor-version":[{"id":3014,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/708\/revisions\/3014"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=708"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=708"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=708"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}