¿Es interesante considerar la teoría de la modulación de la satisfacción en el contexto de la lógica modal?

Question

Recientemente se han realizado muchos trabajos considerando la satisfabilidad de las fórmulas en teoría específica (teoría de matrices, teoría de vectores de bits). Pero no he encontrado ningún resultado sobre la teoría de la satisfabilidad del módulo en el contexto de la lógica modal? ¿Hay alguna razón? ¿Es útil considerar la lógica modal y la teoría de la modulación de la satisfacción?

Gracias.

Answer 1

Hemos estado trabajando en SMT para lógicas modales, y hemos conseguido demostrar que SMT con cuantificación produce un procedimiento de decisión para la lógica modal básica (BML). Esto no es difícil de demostrar cuando se trabaja con la traducción estándar de la LBM y las reglas de instanciación comunes disponibles en algunos solucionadores de SMT. También tenemos los mismos resultados para otros operadores (operador inverso, operador graduado). En última instancia, nuestro objetivo es demostrar que SMT produce un procedimiento de decisión para todo el fragmento vigilado, lo cual suponemos que es así, pero hasta ahora no hemos conseguido una prueba satisfactoria. En términos de eficiencia, estamos realizando algunas pruebas para ver cómo se comporta un prover de SMT con fórmulas modales. Hasta ahora, no tengo los números.