{"id":1684,"date":"2011-11-15T06:17:20","date_gmt":"2011-11-15T06:17:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalization-of-propositional-linear-temporal-logic-in-the-mizar-system\/"},"modified":"2013-03-08T05:49:00","modified_gmt":"2013-03-08T05:49:00","slug":"resena-formalization-of-propositional-linear-temporal-logic-in-the-mizar-system","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalization-of-propositional-linear-temporal-logic-in-the-mizar-system\/","title":{"rendered":"Rese\u00f1a: Formalization of propositional linear temporal logic in the Mizar system"},"content":{"rendered":"<p>Una l\u00ednea de trabajo dentro del campo del razonamiento formalizado consiste en la formalizaci\u00f3n de la metal\u00f3gica de distintos sistemas l\u00f3gicos. En esta l\u00ednea se inscribe el art\u00edculo <a href=\"http:\/\/bit.ly\/scCQtE\">Formalization of propositional linear temporal logic in the Mizar system<\/a>. <\/p>\n<p>Su autor es <a href=\"http:\/\/www.cs.ru.nl\/~giero\/\">Mariusz Giero<\/a> (University of Bialystok).<\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nThe paper describes formalization of some issues of propositional linear temporal logic (PLTL). We discuss encountered problems and applied solutions. The formalization was carried out in the Mizar system. In comparison with other systems, Mizar is famous for its large repository of computer checked mathematical knowledge and also for its user-friendly knowledge representation and proof language.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Una l\u00ednea de trabajo dentro del campo del razonamiento formalizado consiste en la formalizaci\u00f3n de la metal\u00f3gica de distintos sistemas l\u00f3gicos. En esta l\u00ednea se inscribe el art\u00edculo Formalization of propositional linear temporal logic in the Mizar system. Su autor es Mariusz Giero (University of Bialystok). Su resumen es The paper describes formalization of some&#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":[100],"tags":[188,273,285],"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\/1684"}],"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=1684"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1684\/revisions"}],"predecessor-version":[{"id":2913,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1684\/revisions\/2913"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1684"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1684"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1684"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}