{"id":27,"date":"2008-01-15T15:00:14","date_gmt":"2008-01-15T13:00:14","guid":{"rendered":"https:\/\/blogs.ua.es\/madbinnacle\/2008\/01\/15\/bloque-iv-demostracion-automatica-de-teoremas-dat\/"},"modified":"2008-01-26T22:11:41","modified_gmt":"2008-01-26T20:11:41","slug":"bloque-iv-demostracion-automatica-de-teoremas-dat","status":"publish","type":"post","link":"https:\/\/blogs.ua.es\/madbinnacle\/2008\/01\/15\/bloque-iv-demostracion-automatica-de-teoremas-dat\/","title":{"rendered":"Bloque IV “DEMOSTRACI\u00d3N AUTOM\u00c1TICA DE TEOREMAS” DAT"},"content":{"rendered":"

clase N\u00ba 13, 15 de Enero de 2007, Horario: 15:00 – 17:00, Carlos Villagr\u00e1.<\/i><\/p>\n

\n
\nHoy despu\u00e9s de cuatro meses hemos tenido nuestra \u00faltima clase de l\u00f3gica en la cual tuvimos la explicaci\u00f3n del bloque IV e hicimos el \u00faltimo examinador sobre Deducci\u00f3n Natural.<\/p>\n

Lo que pudimos ver del tema me hace pensar que no es muy dificil deducir argumentos por medio de la Resoluci\u00f3n, pero claro!, hay que tener en cuenta que para poder utilizar este m\u00e9todo antes que todo debemos obtener la Forma Clausual de la f\u00f3rmula, factor que hace un poco desagradable el m\u00e9todo para el caso de f\u00f3rmulas del lenguaje predicativo, que incluye aplicar la forma normal de Prenex<\/i> y de skolem<\/i>, que aunque Prenex no presente dificultad, lo muestra skolem en el caso de encontrarse cuantificadores existenciales en el \u00e1mbito del cuantificador universal; del resto parece ser un m\u00e9todo bastante pr\u00e1ctico.<\/p>\n

<\/br>
\n
<\/br>
\nEl proceso “DAT” para estudiar la validez de un argumento consiste en:<\/p>\n

  • 1\u00ba<\/strong> Formalizar el problema a resolver P1,\u2026,Pn \u21d2 Q. <\/li>\n
  • 2\u00ba<\/strong> Obtener un conjunto de fbfs C formado por todas las “CL\u00c1USULAS”<\/i> que se obtienen de las premisas.<\/li>\n
  • 3\u00ba<\/strong> Negaci\u00f3n de la fbf conclusi\u00f3n (\u00acQ) .<\/li>\n
  • 4\u00ba<\/strong> A\u00f1adir a C las cl\u00e1usulas que se obtienen de \u00acQ<\/li>\n
  • 5\u00ba<\/strong> Demostrar que el conjunto C ={CP1, CP2,\u2026,C\u00acQ} es INSATISFACIBLE<\/i> usando la REGLA DE RESOLUCI\u00d3N DE ROBINSON<\/i>. <\/li>\n

    <\/br>
    \nLa Regla de Resoluci\u00f3n<\/i> dice:<\/p>\n

    Dadas dos cla\u00fasulas que contienen una el literal L y otra \u00acL, es decir de la forma, L v A1, y \u00acL v A2, puede deducirse de ambas la f\u00f3rmula A1 v A2. Esta f\u00f3rmula se llama cl\u00e1usula resolvente<\/strong>, y a las f\u00f3rmulas a las que se les aplica, formulas padres<\/strong>.<\/p>\n

    La clausula resolvente se calcula tomando la disyunci\u00f3n de las dos cl\u00e1usulas y eliminando de ellas el par de complementarios L v \u00acL.<\/p>\n

    Cl\u00e1usulas Padre<\/font><\/p>\n

    [L v A1 v A2 v … v An ] y [ \u00acL v B1 v B2 v … v Bm ]<\/p>\n

    Cl\u00e1usula resolvente<\/font><\/p>\n

    [A1 v … v An v B1 v … v Bm]<\/p>\n

    <\/br>
    \n
    <\/br>
    \nEjemplos:<\/strong>
    \nCl\u00e1usula Padre:<\/i>P y \u00acP v Q
    \nCl\u00e1usula Resolvente:<\/i> Q<\/p>\n

    Cl\u00e1usula Padre:<\/i>P v Q y \u00acP v Q
    \nCl\u00e1usula Resolvente:<\/i> Q<\/p>\n

    Cl\u00e1usula Padre:<\/i>P v Q y \u00acP v \u00acQ
    \nCl\u00e1usula Resolvente:<\/i> Q v \u00acQ, P v \u00ac P <\/p>\n

    Cl\u00e1usula Padre:<\/i> Q y \u00ac Q
    \nCl\u00e1usula Resolvente:<\/i> NADA (La Cl\u00e1usula Vac\u00eda [] significa contradicci\u00f3n)<\/p>\n

    Cl\u00e1usula Padre:<\/i>P v Q Y \u00acP v R
    \nCl\u00e1usula Resolvente:<\/i> Q v R<\/p>\n

    <\/br>
    \nEl siguiente argumento del calculo de proposiciones fu\u00e9 el ejemplo utilizado en clase para demostrar por medio de la Refutaci\u00f3n por Resoluci\u00f3n.<\/p>\n

    (p\u2192q)\u2192r,\u00acp v q \u21d2 r<\/p>\n

    La Forma Clausual de la f\u00f3rmula correspondiente a la afirmaci\u00f3n de las premisas y la negaci\u00f3n de la conclusi\u00f3n es:
    \n[(p \u2192 q) \u2192 r] \u2227 (\u00acp v q) \u2227 \u00ac r
    \n[\u00ac(\u00acp v q) v r] \u2227 (\u00acp v q) \u2227 \u00ac r
    \n[(\u00ac\u00acp \u2227 \u00acq) v r] \u2227 (\u00acp v q) \u2227 \u00ac r
    \n[(p \u2227 \u00acq) v r] \u2227 (\u00acp v q) \u2227 \u00ac r
    \n(p v r) \u2227 (\u00acq v r) \u2227 (\u00acp v q) \u2227 \u00ac r<\/p>\n

    C1: p v r
    \nC2: \u00acq v r
    \nC3: \u00acq v q
    \nC4: \u00acr<\/p>\n

    ej_biv.jpg<\/a><\/p>\n

    En conclusion hemos llegado a la cl\u00e1sula vac\u00eda que no es mas que una prueba de insatisfacibilidad, que demuestra que es correcto el argumento.<\/p>\n

    <\/br>
    \n
    <\/br><\/p>\n

    RESOLUCI\u00d3N EN EL LENGUAJE PREDICATIVO<\/strong><\/div>\n

    UNIFICACI\u00d3N:<\/i>
    \nProceso por el cual mediante sustituci\u00f3n de t\u00e9rminos de variables podemos obtener expresiones id\u00e9nticas y as\u00ed se pueden unificar.<\/p>\n

    Veamos ahora el ejemplo visto en clase.<\/p>\n

    Cualquiera que puede cantar es cantante
    \nLos p\u00e1jaros no son cantantes
    \nAlg\u00fan p\u00e1jaro tiene buena voz
    \nLuego, Alguiennn que tiene buena voz no puede cantar<\/p>\n

    R(x): x puede cantar
    \nC(x): x es cantante
    \nP(x): x es p\u00e1jaro
    \nV(x): x tiene buena voz<\/p>\n

    Formalizamos<\/i>
    \n\u2200x[R(x) \u2192 C(x)]
    \n\u2200x[P(x) \u2192 \u00acC(x)]
    \n\u2203x[P(x) \u2227 V(x)] \u21d2 \u2203x[V(x) \u2227 \u00acR(x)]<\/p>\n

    Convertimos a Forma Clausual:<\/i><\/p>\n

    \u2200x[R(x) \u2192 C(x)] \u2227 \u2200x[P(x) \u2192 \u00acC(x)] \u2227 \u2203x[P(x) \u2227 V(x)] \u2227 \u00ac\u2203x[V(x) \u2227 \u00acR(x)]<\/p>\n

    C1: \u00acR(x) v C(x)
    \nC2: \u00acP(y) v \u00acC(y)
    \nC3: P(a)
    \nC4: V(a)
    \nC5: \u00acV(z) v R(z)
    \n    ej2_biv.jpg<\/a><\/p>\n

    Por \u00faltimo enlazo el examinador de Deduccion Natural, con la soluci\u00f3n de Carlos:Control Bloque III.<\/a>
    \n<\/font>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

    clase N\u00ba 13, 15 de Enero de 2007, Horario: 15:00 – 17:00, Carlos Villagr\u00e1. Hoy despu\u00e9s de cuatro meses hemos tenido nuestra \u00faltima clase de l\u00f3gica en la cual tuvimos la explicaci\u00f3n del bloque IV e hicimos el \u00faltimo examinador sobre Deducci\u00f3n Natural. Lo que pudimos ver del tema me hace pensar que no es […]<\/p>\n","protected":false},"author":160,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[782,318],"tags":[],"class_list":["post-27","post","type-post","status-publish","format-standard","hentry","category-bloque-iv-dat","category-clases-teoricas"],"_links":{"self":[{"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/posts\/27","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/users\/160"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/comments?post=27"}],"version-history":[{"count":0,"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/posts\/27\/revisions"}],"wp:attachment":[{"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/media?parent=27"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/categories?post=27"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.ua.es\/madbinnacle\/wp-json\/wp\/v2\/tags?post=27"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}