A Dual-Context Sequent Calculus for S4 Modal Lambda-Term Synthesis

Artículo académico que aborda el problema de habitabilidad/síntesis en el caso de tipos modales dentro del fragmento de necesidad de la lógica constructiva S4. El enfoque es guiado por humanos, en el sentido de los procedimientos de razonamiento típicos de los demostradores automáticos de teoremas modernos. Para ello, se emplea el llamado "cálculo de secuentes de doble contexto", en el que los secuentes tienen dos contextos, propuesto originalmente para capturar las nociones de verdades globales y locales sin recurrir a una semántica formal.