Artículo de revista
Semánticas de punto fijo para programas anotados. Una realización por Mho-resolución.
Autor
Ramírez, Carlos Ernesto
Institución
Resumen
En programación lógica clásica, una de las herramientas conceptuales más poderosas consiste
en la interpretación semántica de un conjunto de fórmulas como funciones sobre conjuntos
ordenados con ciertas propiedades estructurales. Tales funciones en combinación con teoremas de
punto fijos como el de Knaster-Tarsky permite resolver ecuaciones de definición en la semántica
declarativa de un programa lógico, dando origen a una semántica completa para el programa. En
este trabajo, a través de un operador de consecuencia basado en una técnica de hiper-resolución anotada conocida como f-resolución, introducimos una semántica de punto fijo para programas lógicos anotados.