{"id":3711,"date":"2013-10-01T08:06:30","date_gmt":"2013-10-01T06:06:30","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3711"},"modified":"2013-10-01T08:10:27","modified_gmt":"2013-10-01T06:10:27","slug":"the-ontological-argument-in-pvs","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/the-ontological-argument-in-pvs\/","title":{"rendered":"The ontological argument in PVS"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/pvs.csl.sri.com\">PVS<\/a> titulado <a href=\"http:\/\/www.csl.sri.com\/users\/rushby\/papers\/ontological.pdf\">The ontological argument in PVS<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.csl.sri.com\/users\/rushby\">John Rushby<\/a> (del <i>SRI International<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThe <a href=\"http:\/\/en.wikipedia.org\/wiki\/Ontological_argument\">Ontological Argument<\/a>, an 11th Century proof of the existence of God, is a good candidate for <a href=\"http:\/\/www.iis.nsk.su\/fwfm2013\">Fun With Formal Methods<\/a> as nearly everyone finds the topic interesting. We formalize the Argument in <a href=\"http:\/\/pvs.csl.sri.com\">PVS<\/a> and verify its correctness. The formalization raises delicate questions in formal logic and provides an opportunity to show how these are handled, soundly and efficiently, by the predicatively-subtyped higher-order logic of PVS and its mechanized support. The simplicity of the Argument, coupled to its bold conclusion, raise interesting issues on the interpretation and application of formal methods in the real world.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en PVS titulado The ontological argument in PVS. Su autor es John Rushby (del SRI International). Su resumen es The Ontological Argument, an 11th Century proof of the existence of God, is a good candidate for Fun With Formal Methods as nearly everyone finds the topic interesting&#8230;.<\/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":[21,100],"tags":[277,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\/3711"}],"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=3711"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3711\/revisions"}],"predecessor-version":[{"id":3716,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3711\/revisions\/3716"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3711"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3711"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3711"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}