Hipersecuentes: asignaciones de términos de prueba o traducciones a lógica híbrida

He estado mirando una lógica modal con el axioma

Aproximadamente, esto dice que la relación de accesibilidad es lineal.

Parece que puedes dar una teoría de prueba para este lenguaje usando hipersecuentes (ver Cálculo de hipersecuencia libre de corte de Andrzej Indrzejczak para S4.3 ), y me preguntaba si alguien ha investigado dar asignaciones de términos de prueba a cálculos hipersecuentes.

Alternativamente, estaría igual de feliz si alguien hubiera mostrado cómo traducir cálculos hipersecuentes en lógicas híbridas.

Cualquier puntero?

Sé que esto es un poco tarde, pero quizás aún sea de interés.

Si bien no es exactamente la lógica que le interesa, la lógica de Gödel-Dummett, la lógica intermedia caracterizada por marcos lineales de Kripke, está estrechamente relacionada con S4.3, y para esta lógica la gente ha investigado preguntas similares:

• El artículo A Lambda Calculus for Goedel-Dummett Logic Capturing Watifreedom de Yoichi Hirai da un cálculo lambda basado en un cálculo hipersecuente para esa lógica.

• El documento A Natural Deduction System for Intuitionistic Fuzzy Logic por Matthias Baaz, Agata Ciabattoni y Christian Fermüller ofrece un sistema de deducción natural para la misma lógica, que podría usarse para dar asignaciones de términos de prueba.

Además, es posible que le interese el artículo De las propiedades del marco a las Reglas hipersecuentes en lógicas modales de Ori Lahav, que incluye un cálculo hipersecuente alternativo para S4.3.