Un ejemplo simple de lógica cautelosa es el siguiente: si X es verdadero, entonces Y, de lo contrario, Z puede expresarse en lógica dinámica como (X?; Y) ∪ (~ X?; Z). Esto muestra una elección lógica cautelosa: si X se cumple, entonces X?; Y es igual a Y, y ~ X?; Z está bloqueado, y el bloque Y∪ también es igual a Y. Por lo tanto, cuando X es verdadero, el ejecutante principal de la acción solo puede tomar la rama Y, y cuando es falsa, la rama Z. [1]
Un ejemplo del mundo real es la idea de paradoja : algo no puede ser tanto verdadero como falso. Una elección lógica cautelosa es aquella en la que cualquier cambio en la verdad afecta a todas las decisiones tomadas en el futuro. [2]
Antes del uso de la lógica cautelosa, se usaban dos términos principales para interpretar la lógica modal. La lógica matemática y la teoría de bases de datos (Inteligencia Artificial) eran la lógica de predicados de primer orden. Ambos términos encontraron subclases de lógica de primera clase y se usaron de manera eficiente en lenguajes solubles que se pueden usar para la investigación. Pero ninguno de los dos podría explicar las poderosas extensiones de punto fijo a las lógicas de estilo modal.
Más tarde, Moshe Y. Vardi [3] hizo una conjetura de que un modelo de árbol funcionaría para muchas lógicas de estilo modal. El fragmento cauteloso de lógica de primer orden fue introducido por primera vez por Hajnal Andréka , István Németi y Johan van Benthem en su artículo Lenguajes modales y fragmentos acotados de lógica de predicados. Transfirieron con éxito propiedades clave de lógica descriptiva , modal y temporal.predicar la lógica. Se encontró que la decidibilidad robusta de la lógica protegida podría generalizarse con una propiedad de modelo de árbol. El modelo de árbol también puede ser una fuerte indicación de que la lógica protegida extiende el marco modal que conserva los conceptos básicos de las lógicas modales.
Las lógicas modales se caracterizan generalmente por invariancias bajo bisimulación . También sucede que la invariancia bajo bisimulación es la raíz de la propiedad del modelo de árbol que ayuda a definir la teoría de los autómatas .
Dentro de Guarded Logic existen numerosos objetos protegidos. El primero es un fragmento protegido que son lógicas de primer orden de la lógica modal. Los fragmentos protegidos generalizan la cuantificación modal al encontrar patrones relativos de cuantificación. La sintaxis utilizada para denotar el fragmento protegido es GF . Otro objeto es la lógica de punto fijo protegido denotado μGF naturalmente extiende el fragmento protegido desde los puntos fijos de menor a mayor. Las bisimulaciones guardadas son objetos que al analizar la lógica guardada. Todas las relaciones en un álgebra relacional estándar ligeramente modificada con bisimulación protegida y definible de primer orden se conocen como álgebra relacional protegida . Esto se denota mediante GRA .