Negación Constructiva para Programación Lógica Ecuacional

Dentro del campo de los lenguajes ecuacionales y lógico- ecuacionales, una de las extensiones en la que últimamente
se han centrado las investigaciones es la incorporación de la negación. Esta extensión
no sólo incrementa la potencia expresiva de los lenguajes sino que es necesaria para poder expresar
algunos problemas cuya formulación más natural hace uso de la negación, como es el caso de las especificaciones de algunos tipos de datos.

El problema de la negación del predicado igualdad se ha abordado con técnicas y planteamientos muy distintos.
Así, por ejemplo, algunas aproximaciones abordan el problema de resolver la desigualdad con respecto a la teoría ecuacional vacía.
Otras consideran sistemas de ecuaciones y disecuaciones a resolver con respecto a teorías ecuacionales de Horn
satisfaciendo diversas restricciones. Finalmente, otras propuestas (entre las que podemos situar la presentada en esta tesis) consideran teorías ecuacionales que incluyen negación,
con respecto a las que se resuelven sistemas de ecuaciones o sistemas de ecuaciones y disecuaciones (como es nuestro caso) usando diversos mecanismos operacionales basados
o en la reescritura de términos o en algún procedimiento de resolución de ecuaciones (tal y como narrowing).
Quizás algunas de las causas que han contribuido a esta diversidad de planteamientos son la propia complejidad del predicado igualdad y la existencia de problemas abiertos dentro del campo de las especificaciones positivas.

El principal argumento discutido en esta tesis es que es posible resolver constructivamente la negación del predicado igualdad.
El término constructivo hace referencia a una de las aproximaciones propuestas para resolver la negación en programación lógica
y que fue acu&~n;ada bajo el apelativo de Negación Constructiva. Esta denominación alude directamente
a la forma en que se tratan los literales negados: en esta aproximación, las respuestas a un literal negado
son construidas a partir de las respuestas de su versión positiva. Siguiendo esta idea, en la tesis se define una extensión del algoritmo
de narrowing capaz de resolver conjunciones de ecuaciones y disecuaciones con respecto a una teoría ecuacional
de Horn que permite el uso de disecuaciones en las condiciones de las cláusulas. Uno de los atractivos de nuestra aproximación es que el mecanismo computacional subyacente
es único ya que la resolución de una disecuación se obtiene como una adecuada transformación
de una subderivación para su versión positiva que define la regla de negación constructiva ecuacional.
Otra de sus características, en relación a otras propuestas, es la presencia en las respuestas computadas de variables cuantificadas universalmente, que surgen como resultado del proceso de transformación aplicado cuando se resuelven subobjetivos negados.