Semántica funcional para lógicas temporales X modales. Definibilidad y Teoremas de completitud

Abstract

Este trabajo está enmarcado en un área de conocimiento teórico, concretamente en el campo de la Lógica Formal como parte de los Fundamentos Matemáticos de la Computación. Sin embargo, su motivación ha partido de un área de conocimiento aplicado como la búsqueda de lógicas adecuadas para la especificación y control de procesos y sistemas multiagentes. Las lógicas introducidas permiten la especificación y control de procesos paralelos y el comportamiento de distintos agentes conectados en red. La investigación llevada a cabo por nuestro grupo de investigación GIMAC (Grupo de Investigación en herramientas matemáticas para la Computación) hasta la fecha de inicio de este trabajo, cuyo objetivo puede ser descrito como: "El diseño de una nueva metodología de demostración automática de teoremas que contribuya al uso real de software deductivo y, en definitiva, al uso de la Lógica en Computación" y, concretamente, los estudiso realizados en el grupo en aspectos tanto teóricos como aplicativos de las lógicas modales y temporales, y siendo conscientes de que las aplicaciones reclaman la integración de distintas lógicas, planteamos lógica adecuada a las aplicaciones anteriormente señaladas una lógica temporal x modal. Consideramos como aspectos destacado y novedosos en la investigación: El estudio de la definibilidad de las propiedades destacadas de clases de funciones tales como: totalidad, sobreyectividad, inyectividad, crecimiento, componibilidad, sin necesidad de hacer uso de la lógica de segundo orden. Deseamos destacar que nuestro trabajo ha tenido un punto de partida diferente a la de los trabajos existentes en la bibliografía en los que encontramos contemplada la combinación de tiempo y modalidad y en los que se abordan cuestiones filosóficas tales como el determinismo, la teoría de la acción, la causalidad, los condicionales, etc. Ver, por ejemplo, [Aqvist(1999)], [Belnap and Perloff)1990)], [Beln