Home

en otra ventana

1. S Los precios bajan U La mayor a de la gente no es feliz Hay cuatro enunciados en este ejemplo los cuales son 1 Si la tasa de inter s sube los precios bajan 2 Si los precios bajan la mayor a de la gente no es feliz 3 La tasa de inter s sube 4 La mayor a de la gente no es feliz Ahora si nosotros queremos demostrar que 4 es verdadera si 1 1 2 A 3 son verdaderas Por lo que formalizamos nuestras premisas y establecemos las sentencias relevantes 1 P gt S8 2 5S gt U 3 P Necesitamos derivar 4 U Por lo que se requiere realizar un archivo de tipo texto con lo siguiente set binary_res set process_input clear print_kept clear print_back_sub assign max_mem 1500 1 5 Megabytes formula_list sos problem P gt SUN P goal U end_of_ list Dentro del archivo de salida contiene la siguiente demostraci n PROOF 25 LA SP Sa 2 1 S U 3 P 4 U 5 binaryy dad 3 LS 6 binary 2 1 5 1 U 7 binary 6 1 4 1 F nd of proof Por lo que podemos concluir que la mayor a de la gente no es feliz Ejemplo 3 2 Problema de S ntesis Qu mica Cha87 Supongamos que podemos ejecutar las siguientes reacciones qu micas e MgO H gt Mg H20 e C 0 C0 o CO HO gt HCO Suponga que tenemos algunas cantidades de MgO H2 O2 y C Muestre que podemos hacer H2C0O3 Para este problema podemos
2. ado para ejecutarse en ambiente UNIX aunque existen versiones limitadas que se pueden ejecutar bajo los sistemas operativos DOS o Macintosh OTTER lee un archivo de entrada que contiene un conjunto de f rmulas o cl usulas de l gica de primer orden con igualdad dividido en listas y alguna informaci n extra para controlar la ejecuci n El conjunto de f rmulas incluye las hip tesis y la negaci n de la conclusi n todas las pruebas son por contradicci n la informaci n de control consiste de diversos par metros y banderas que especifican las reglas de inferencia que se utilizar n y las estrategias de b squeda Mientras OTTER busca va escribiendo la informaci n obtenida a un archivo de salida incluyendo la refutaci n buscada si sta ocurri Las f rmulas se construyen con los s mbolos listados en la tabla 3 1 Interpretaci n S mbolo Negaci n Conjunci n amp Disyunci n l Implicaci n gt Equivalencia lt gt Cuantificaci n existencial exists Cuantificaci n universal all Igualdad Desigualdad l Tabla 3 1 S mbolos con que se construyen las f rmulas en OTTER 22 Las reglas de inferencia que OTTER conoce son resoluci n binaria hiperresoluci n hiperresoluci n negativa y UR resoluci n Mediante el comando set r se le indica al programa que regla de inferencia usar y mediante el comando clear r se le indica que regla dejar de usar Aqu r puede ser simbo
3. considerar MGO H2 O2 y C como f rmulas at micas Luego las reacciones qu micas de arriba pueden ser representadas por las siguientes f rmulas Al MGO H2 MG H20 A2 C 102 gt CO2 A3 CO2 H20 gt H2C03 Dado que tenemos MGO H2 O2 y C estos factores pueden ser representados por las siguientes f rmulas A4 MGO A5 H2 A6 O2 A7 C Ahora el problema puede ser visto de la siguiente manera c mo probar que H2C0O3 es una consecuencia l gica de A1 A7 Para lo que se requiere realizar un archivo de tipo texto con lo siguiente sel sel binary_res process_input 26 clear print_kept clear print_back_sub assign max_mem 1500 1 5 Megabytes formula_list sos problem MGO H2 gt MG H20 C 02 gt CO2 CO2 H20 gt H2C03 MGO H2 02 ae goal H2C03 end_of_list Dentro del archivo de salida se encuentra la siguiente demostraci n PROOF 2 MGO H2 H20 3 E 02 602 4 CO2 H20 H2C03 5 MGO 6 H2 7 02 8 EN 9 H2C03 11 binary 2 1 5 1 unit_del 6 H20 12 binary 3 1 8 1 unit_del 7 CO2 13 binary 4 1 12 1 unit_del 11 9 F nd of proof Por lo que podemos concluir que H2CO es una consecuencia l gica de Al A7 Ejemplo 3 3 Gen88 Consideremos el siguiente problema Conocemos que los caballos son m s r pidos que los perros y que hay un galgo que es m
4. s r pido que cada conejo Conocemos que Harry es un caballo y que Ralph es un conejo Nuestro trabajo va a ser demostrar el hecho que Harry es m s r pido que Ralph Primero necesitamos formalizar nuestras premisas Las sentencias relevantes son las siguientes V x V y Caballo x amp Perro y Mas_R pido x y 27 V y Galgo y amp VY z Conejo z Mas_R pido y z V y Galgo y Perro y Vx V y V z Mas_R pido x y amp Mas_R pido y z Mas_R pido x z Caballo Harry Conejo Ralph Note que estamos adicionando dos hechos acerca del mundo no establecidos expl citamente en el problema que los galgos son perros y que nuestra velocidad de relaci n es transitiva Y que lo que necesitamos derivar es lo siguiente Mas_R pido Harry Ralph Por lo que tenemos que realizar una archivo de tipo texto con lo siguiente set binary_res set process_input clear print_kept clear print_back_sub assign max_mem 1500 1 5 Megabytes formula_list sos problem all x all y caballo x perro y gt mas_rapido x y exists y galgo y all z conejo z gt mas_rapido y Zz all y galgo y gt perro y all x all y all z mas_rapido x y mas_rapido y z gt mas_rapido x z caballo Harry conejo Ralph goal mas_rapido Harry Ralph end_of_list El cual al indicarlo como archivo de entrada en OTTER obtenemos la prueba del teorema en el archivo de sal
5. Cap tulo 3 Razonamiento Autom tico en OTTER En este cap tulo presentaremos una breve descripci n de lo que es OTTER y su importancia Tambi n se presenta informaci n sobre su estrategia de razonamiento arquitectura y su proceso de inferencia junto con algunos ejemplos de c mo trabaja Cabe aclarar que no se pretende dar informaci n muy detallada ni un tutorial sobre el manejo de esta herramienta Para conocer a fondo todas las funciones del programa consulte la referencia McC94 y para encontrar un tutorial b sico v ase la referencia Wos92 Si el lector est interesado en un tutorial avanzado es recomendable la referencia Wos96 3 1 Qu es OTTER OTTER es un demostrador autom tico que implementa el m todo de resoluci n para l gica de primer orden con igualdad Fue desarrollado en el Laboratorio Nacional de Argonne USA Las siglas OTTER significan Organized Techniques for Theorem proving and Effective Research Las condiciones primarias para su dise o fueron el desarrollo la portabilidad y la extensibilidad Amo98 Para mas informaci n consulte las referencias McC94 Amo98 y Mir99 18 3 2 Importancia de OTTER OTTER tiene una efectividad extraordinaria y ha resuelto problemas abiertos en diversas reas como Teor a de grupos Geometr a Algebraica Algebras Booleanas Teor a de Ret culos y L gica Combinatoria Amo98 Con OTTER se han logrado obtener resultados que no se hab an podido dem
6. a Por otra parte una de las estrategias m s poderosas de direcci n que son las que dictan hacia donde dirigir la atenci n es la estrategia de peso Un programa de razonamiento autom tico que emplea pesos elige la cl usula con el peso m s favorable en el caso de OTTER se prefieren cl usulas m s ligeras es decir cl usulas con menor peso OTTER tambi n ofrece una t cnica efectiva para b squeda de pruebas cortas conocida como la estrategia de la raz n que fue formulada para escoger que cl usula debe ser la siguiente en procesar Aunque el peso es de gran utilidad para guiar la b squeda de un programa su uso retrasa y hasta evita el procesamiento de cl usulas muy pesadas Una manera para seleccionar con anticipaci n cl usulas pesadas es utilizar la b squeda a lo ancho Sin embargo una b squeda a lo ancho obliga al programa a escoger en cada nivel un n mero mayor de cl usulas Para combinar las dos estrategias tenemos la estrategia de la raz n que dado un entero k causa que el programa elija para procesar k cl usulas por peso y despu s una por cada nivel El estudio de nuevas y mejores estrategias es de gran importancia y es uno de los principales temas de investigaci n actualmente Mir99 21 3 5 Arquitectura de OTTER OTTER est escrito en lenguaje de programaci n C el cual proporciona velocidad y portabilidad Consta aproximadamente de 35 000 l neas de c digo incluyendo comentarios Est dise
7. iclo de inferencia principal es el algoritmo de la cl usula dada que opera en las listas sos y usable While sos Sea Cd la cl usula mas ligera de sos sos sos Cd usable usable U Cd Infiere Cd End While Donde el proceso Infiere Cd genera nuevas cl usulas utilizando las reglas de inferencia en acci n con la condici n de que cada cl usula nueva debe tener a ca como uno de sus padres y elementos de la lista usable como sus padres restantes Adem s las nuevas cl usulas se someten a pruebas de retenci n y aqu llas que sobreviven se agregan a la lista sos 3 7 Ejemplificaci n de OTTER A continuaci n se muestra una ejemplificaci n b sica de como funciona la herramienta OTTER Para informaci n sobre c mo utilizarla consultar el Ap ndice A Primeramente se da una redacci n de cada ejemplo a demostrar despu s se traducen los enunciados de cada prueba a su forma clausular para despu s introducirlos dentro del archivo de entrada de OTTER y por ltimo se muestra la parte de prueba del archivo de salida que infiere OTTER Ejemplo 3 1 Cha87 Supongamos que los precios bajan si la tasa de inter s sube Suponga tambi n que la mayor a de la gente no es feliz cuando los precios bajan Asuma que la tasa de inter s sube Muestre que se puede concluir que la mayor a de la gente no es feliz Perm tanos denotar los enunciados mencionados como sigue 24 P Sube la tasa de inter s
8. ida el cual contiene entre otras cosas la derivaci n de c mo el teorema fue demostrado tal como se muestra a continuaci n PROOF caballo x perro y mas_rapido x y galgo cl1 galgo x perro x 0 e 0 NR conejo x mas_rapido c1 x mas_rapido x y mas_rapido y z mas_rapido x z 28 0 0 JJ 0 10 11 16 19 36 37 co ina bin bin caballo Harry nejo Ralph as_rapido Harry Ralph ry 4 1 2 1 perro cl ary 3 1 7 1 mas_rapido c1 Ralph ary 1 1 6 1 perro x mas_rapido Harry xX ary 11 1 9 1 mas_rapido Harry c1 ary 3 16 LI mas_rapido c1 x mas_rapido Harry x ary 19 1 10 1 mas_rapido Harry Ralph ary 36 1 8 1 F nd of proof Por lo que podemos concluir que Harry es m s r pido que Ralph 29
9. lizada por bynary_res hyper_res neg_hyper_res ur_res para_into para_from y demod_info para habilitar la bandera de resoluci n binaria hiperresoluci n hiperresoluci n negativa resoluci n UR paramodulaci n o demodulaci n respectivamente 3 6 El proceso de Inferencia de OTTER OTTER trabaja con cl usulas nicamente pero es posible proporcionarle f rmulas cualesquiera como entrada Estas f rmulas ser n transformadas autom ticamente a forma clausular El mecanismo b sico de inferencia de OTTER es el algoritmo de la cl usula dada que se puede ver como una implementaci n de la estrategia del conjunto de soporte OTTER mantiene cuatro listas de cl usulas que se encuentran en la tabla 3 2 Tipo de Lista de Cl usulas usable En la lista est n disponibles para hacer inferencia sos Es la lista del conjunto de soporte set of support las cl usulas de esta lista no est n disponibles para hacer inferencias por s solas est n esperando para participar en b squeda de una refutaci n passive Las cl usulas de esta lista no participan directamente en la b squeda se usan nicamente para subsunci n y conflicto de unidades Esta lista est fija desde el inicio y no cambia durante el proceso demulators Aqu est n los demuladores que se usan para reescribir las cl usulas inferidas Tabla 3 2 Lista de cl usulas que mantiene OTTER 23 Algunas de estas listas pueden estar vac as El c
10. maci n adicional con respecto a la demostraci n de OTTER se encuentra disponible en la referencia Http1 3 3 2 Nuevas Resultados obtenidos a trav s de OTTER En el Laboratorio Argonne de Estados Unidos se han obtenido nuevos resultados en el rea de razonamiento autom tico La principal contribuci n de estos programas es que ayudan a pruebas manuales encontrando una prueba sin gu a del usuario En la p gina Http2 se encuentra un resumen de tales resultados de los cuales varios fueron obtenidos a trav s de OTTER 3 4 Estrategia de razonamiento en OTTER Para que un programa de razonamiento autom tico sea efectivo se requiere del uso de estrategias Una estrategia es una serie de metarreglas que gu an la aplicaci n de las reglas de inferencia Si una estrategia decide que regla de inferencia debe aplicarse en cierto momento del proceso decimos que es una estrategia de direcci n Si una estrategia evita el uso de ciertas reglas de inferencia entonces decimos que es una estrategia de 20 restricci n Ambos tipos de estrategia son necesarios para la efectividad de un programa de razonamiento autom tico Mir99 Entre las estrategias de restricci n una de las m s poderosas es la estrategia de soporte la cual le prohibe a un programa de razonamiento autom tico aplicar una regla de inferencia a menos que uno de los padres o premisas se haya deducido o sea miembro de un conjunto distinguido de cl usulas de entrad
11. ostrar por m todos tradicionales Adem s en lo que se refiere a concursos de razonamiento autom tico OTTER ha destacado entre los primeros lugares fue ganador de la divisi n ecuacional en CASC 13 3 3 Aplicaciones relevantes Se describen dos aplicaciones que consideramos relevantes debido a que han sido estudiadas desde hace muchos a os y no se hab an podido demostrar y con OTTER es posible su demostraci n 3 3 1 El problema de Robbins El problema de Robbins Todas las lgebras de Robbins son Booleanas ha sido resuelto cada lgebra de Robbins es Booleana Este problema se ha estudiado desde 1930 y hasta el a o de 1996 se logr demostrar utilizando EQP Equational Prover un programa de demostraci n autom tica muy similar a OTTER La b squeda exitosa tom cerca de 8 d as sobre un procesador RS 6000 y us cerca de 20 megabytes de memoria 19 Considerando que las pruebas encontradas por programas son siempre cuestionables es importante contar con un demostrador autom tico que construya un objeto de prueba detallado junto con un programa simple que controle que el objeto de prueba resulte ser correcto EQP a n no es capaz de construir objetos de prueba as que la prueba de EQP fue utilizada para guiar a OTTER a una prueba del mismo teorema OTTER produjo un objeto de prueba el cual fue controlado a trav s de un inspector de prueba El archivo de entrada la prueba el objeto prueba e infor

en otra ventana

Contents

Download Pdf Manuals

Related Search

Related Contents