Estoy buscando trabajo en sistemas que sean similares a los secuenciantes de orden superior de K. Dosen ("Sistemas secuenciales para lógica modal", JSL 50 ). El único trabajo que conozco es el reciente trabajo de Iemhoff y Metcalfe ("Teoría de la prueba de reglas admisibles", Annals of Pure and Applied Logic 159 (1-2), 2009).
¿Hay otros documentos sobre tales sistemas?
Respuestas:
Nuevamente, no estoy exactamente seguro de lo que está buscando porque hay potencialmente muchos sistemas "similares", pero para trabajos recientes que creo que están muy relacionados, puede leer la Parte II ("Mezcla de derivabilidad y admisibilidad") de la tesis de Dan Licata , así como la lógica de demostrabilidad constructiva de Rob Simmons y Bernardo Toninho.
fuente
No puedo encontrar el documento en línea, pero adivinando en base a las referencias, el sistema de Dosen cambia el contexto de una secuencia o un conjunto múltiple a una estructura gráfica más general. Esto recuerda a varias cosas.
La lógica de visualización de Belnap, en la que muchos conectivos (y no solo conjunción / disyunción) se internalizan en la estructura secuencial.
También recuerda a la deducción etiquetada, en la que la estructura del gráfico se simula agregando etiquetas a las hipótesis y juicios, y requiere un acuerdo entre los dos para descargar una hipótesis. La tesis doctoral de Alex Simpson investiga las aplicaciones de estos sistemas a la lógica modal.
Noam Zeilberger ha investigado las interpretaciones de la regla omega de Buchholz (y las generalizaciones de la misma) como una regla de inferencia literalmente de orden superior, en la que la premisa de una regla se convierte en una función (es decir, un objeto de orden superior) que genera las premisas. Vea su artículo de POPL 2008 "Focusing and Higher-Order Abstract Syntax".
fuente
Mire la encuesta de cálculo de pruebas para la lógica modal en el capítulo 3 de la tesis de maestría de Phiniki Stouppa El diseño de teorías de prueba modal: el caso de S5 .
IIRC, discutió cómo 11 sistemas manejaron la formalización de S5.
fuente