Programación en lógica rebatible: una semántica declarativa

Abstract

La Programación en Lógica Rebatible [GS99, GSC98, Gar00] (de ahora en más P.L.R.) es una extensión de la Programación en Lógica (P.L.) con una nueva clase de reglas, las reglas rebatibles. Estas reglas permiten representar conocimiento tentativo, aumentando, de este modo, el poder expresivo de la P.L.. El razonamiento no monotónico basado en el análisis dialéctico constituye la semántica operacional de la P.L.R.. Para verificar si una consulta es consecuencia de un programa lógico rebatible, este formalismo utiliza un análisis dialéctico de argumentos y contraargumentos. Así, una consulta q tendrá éxito si existe un argumento A de q que lo justifique, i.e., no existen contraargumentos que derroten a A . Ya que los derrotadores son también argumentos podrían existir derrotadores para éstos últimos y así sucesivamente. En los últimos años, la semántica operacional de la P.L.R. ha sido estudiada desde un punto de vista declarativo [Dun95, KT99, JV99, CDSS00], con el objeto de determinar el significado preciso de un programa lógico sin recurrir al control del sistema. El propósito principal de dicho estudio es ayudar al programador a especificar el conocimiento y razonar a partir de él independientemente de cualquier implementación. Por otra parte, la definición de una semántica declarativa ayudará a caracterizar el comportamiento de los programas lógicos rebatibles como sistema de razonamiento no monótono, a través del conjunto de sus consecuencias y compararlo [Dix95a, Dix95b, Dix95c, CDSS00] con otros sistemas de razonamiento, mostrando ventajas y desventajas. En [CS99,CS00a,CS00b], se introdujo una semántica declarativa trivaluada GS basada en juegos que permite modelar la semántica operacional de la P.L.R., en donde el criterio para decidir entre argumentos contradictorios no permite elementos incomparables. Aunque dicha semántica modela el análisis dialéctico, la noción de argumento quedó indefinida. En otras palabras, se asume que el conjunto de argumentos para un literal es dado por algún oráculo. El hecho de considerar a los argumentos como entidades abstractas cuyos roles están determinados por alguna relación de ataque entre argumentos, es común a la mayoría de las semánticas declarativas ya existentes [Dun95]. Esto motivó una caracterización declarativa de la definición procedural de argumento. El estudio presentado en [CS00c] está basado en un concepto introducido, en primer instancia por Tarski para la lógica clásica y, luego adaptado por Lifschitz para programas lógicos básicos. El objetivo de este trabajo es presentar la estructura final de la semántica declarativa trivaluada GS a través de la que se determina el conjunto de las consecuencias de un programa lógico rebatible donde los argumentos también son analizados de una forma declarativa.