Semánticas de punto fijo para programas anotados. Una realización por Mho Resolución

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.