Un método formal que aumenta las fórmulas sintácticas con etiquetas explícitas (por ejemplo mundos, estados, recursos o anotaciones de prueba) que transportan información semántica y guían la aplicación de reglas de inferencia sintácticas.

Principio

Adjuntar anotaciones semánticas mínimas en forma de etiquetas a objetos sintácticos para que la aplicación de reglas y la composición de pruebas sean operaciones locales dirigidas por la sintaxis y reguladas por reglas de manipulación de etiquetas.

Demostración

En lógica modal, cada fórmula se empareja con una etiqueta de mundo w y las reglas permutan o relacionan etiquetas (wRv) para simular accesibilidad; un secuente como w:A, wRv ⊢ v:B hace explícita la semántica de □ y ◇ en los pasos de prueba.

Aplicación incorrecta

Tratar las etiquetas solo como etiquetas cosméticas y no imponer restricciones sobre ellas conduce a pruebas no válidas donde se ignoran relaciones semánticas (por ejemplo accesibilidad o consumo de recursos).

Consecuencia

Usada correctamente, la deducción etiquetada produce sistemas de pruebas más próximos a los modelos semánticos, permite aplicación local de reglas, facilita extensiones modulares para nuevas modalidades o recursos y a menudo simplifica la eliminación de cortes o la extracción de contraejemplos.

Inversión

La inversión es la deducción puramente sintáctica sin etiquetas, donde las reglas deben rastrear implícitamente condiciones semánticas de forma global; esto puede hacer a los sistemas menos modulares y aumentar la no determinismo en la búsqueda de pruebas.

Límite

Se aplica a lógicas cuya estructura semántica puede codificarse como un álgebra finita de etiquetas o como restricciones relacionales; excluye enfoques que requieran evaluación semántica completa en cada paso (por ejemplo verificación de modelos intensiva) en lugar de manipulación simbólica de etiquetas.

Tensión semántica

Existe tensión entre sistemas con muchas etiquetas que exponen detalles semánticos en las pruebas y cáculos etiquetados que mantienen las etiquetas mínimas para preservar la elegancia sintáctica; más etiquetas mejoran la fidelidad semántica a costa de mayor complejidad de prueba.

Síntesis

La deducción etiquetada integra la contabilidad semántica en la sintaxis mediante etiquetas, cambiando apelaciones semánticas globales por transformaciones locales y dirigidas por reglas que hacen explícito y modular el razonamiento sobre modalidades, recursos o estados.