Marco lógico

En lógica , un marco lógico proporciona un medio para definir (o presentar) una lógica como una signatura en una teoría de tipos de orden superior , de tal manera que la demostrabilidad de una fórmula en la lógica original se reduce a un problema de habitabilidad de tipos en la teoría de tipos del marco. ^{[ 1 ] [ 2 ]} Este enfoque se ha utilizado con éxito para la demostración automatizada (interactiva) de teoremas . El primer marco lógico fue Automath ; sin embargo, el nombre de la idea proviene del más conocido Marco Lógico de Edimburgo, LF . Varias herramientas de demostración más recientes, como Isabelle, se basan en esta idea. ^{[ 1 ]} A diferencia de una incrustación directa, el enfoque del marco lógico permite incrustar muchas lógicas en el mismo sistema de tipos. ^{[ 3 ]}

El marco lógico se basa en un tratamiento general de la sintaxis, las reglas y las demostraciones mediante un cálculo lambda con tipos dependientes . La sintaxis se trata de forma similar, pero más general, al sistema de aridades de Per Martin-Löf .

Para describir un marco lógico, se debe proporcionar lo siguiente:

1. Una caracterización de la clase de lógicas de objetos que se van a representar;
2. Un metalenguaje apropiado;
3. Una caracterización del mecanismo mediante el cual se representan las lógicas de objetos.

Esto se resume en:

" Marco de trabajo = Lenguaje + Representación ."

En el caso del marco lógico LF , el metalenguaje es el cálculo λΠ . Este es un sistema de tipos de funciones dependientes de primer orden que se relacionan, mediante el principio de proposiciones como tipos, con la lógica mínima de primer orden . Las características clave del cálculo λΠ son que consta de entidades de tres niveles: objetos, tipos y clases (o familias de tipos). Es predicativo , todos los términos bien tipados son fuertemente normalizadores y Church-Rosser , y la propiedad de ser bien tipado es decidible . Sin embargo, la inferencia de tipos es indecidible.

Una lógica se representa en el marco lógico LF mediante el mecanismo de representación de juicios como tipos. Esto está inspirado en el desarrollo que Per Martin-Löf hizo de la noción de juicio de Kant en las Conferencias de Siena de 1983. Los dos juicios de orden superior, el hipotético${\displaystyle J\vdash K}$y el general,${\displaystyle \Lambda x\in JK(x)}$, corresponden al espacio de funciones ordinarias y dependientes, respectivamente. La metodología de juicios como tipos consiste en que los juicios se representan como los tipos de sus pruebas. Un sistema lógico${\displaystyle {\mathcal {L}}}$Se representa mediante su signatura, que asigna clases y tipos a un conjunto finito de constantes que representan su sintaxis, sus juicios y sus esquemas de reglas. Las reglas y pruebas de una lógica de objetos se consideran pruebas primitivas de juicios hipotético-generales.${\displaystyle \Lambda x\in CJ(x)\vdash K}$.

El sistema Twelf de la Universidad Carnegie Mellon proporciona una implementación del marco lógico LF . Twelf incluye:

• un motor de programación lógica
• razonamiento metateórico sobre programas lógicos (terminación, cobertura, etc.)
• un demostrador de teoremas metalógico inductivo

• Marco gramatical
• Torniquete (símbolo)

• Frank Pfenning (2002). "Marcos lógicos: una breve introducción". En Helmut Schwichtenberg , Ralf Steinbrüggen (ed.). Prueba y confiabilidad del sistema (PDF) . Saltador . ISBN 978-1-4020-0608-1.
• Robert Harper , Furio Honsell y Gordon Plotkin . Un marco para definir lógicas . Journal of the Association for Computing Machinery, 40(1):143-184, 1993.
• Arnon Avron , Furio Honsell, Ian Mason y Randy Pollack. Uso del cálculo lambda tipado para implementar sistemas formales en una máquina . Journal of Automated Reasoning, 9:309-354, 1992.
• Robert Harper. Una formulación ecuacional de LF . Informe técnico, Universidad de Edimburgo , 1988. Informe LFCS ECS-LFCS-88-67.
• Robert Harper, Donald Sannella y Andrzej Tarlecki. Presentaciones de teoría estructurada y representaciones lógicas . Anales de lógica pura y aplicada, 67(1–3):113-160, 1994.
• Samin Ishtiaq y David Pym. Un análisis relevante de la deducción natural . Journal of Logic and Computation 8, 809–838, 1998.
• Samin Ishtiaq y David Pym. Modelos de recursos de Kripke de un agrupado y tipificado dependiente${\displaystyle \lambda }$-cálculo . Revista de Lógica y Computación 12(6), 1061–1104, 2002.
• Per Martin-Löf. " Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas ". " Revista nórdica de lógica filosófica ", 1(1): 11–60, 1996.
• Bengt Nordström, Kent Petersson y Jan M. Smith. Programación en la teoría de tipos de Martin-Löf . Oxford University Press , 1990. (El libro está agotado, pero se ha puesto a disposición una versión gratuita ).
• David Pym. Una nota sobre la teoría de la demostración de la${\displaystyle \lambda \Pi }$-cálculo . Studia Lógica 54: 199–230, 1995.
• David Pym y Lincoln Wallen . Búsqueda de pruebas en el${\displaystyle \lambda \Pi }$-cálculo . En: G. Huet y G. Plotkin (eds.), Marcos lógicos, Cambridge University Press, 1991.
• Didier Galmiche y David Pym. Búsqueda de pruebas en lenguajes de teoría de tipos: una introducción . Theoretical Computer Science 232 (2000) 5-53.
• Philippa Gardner. Representación de lógicas en la teoría de tipos . Informe técnico, Universidad de Edimburgo, 1992. Informe LFCS ECS-LFCS-92-227.
• Gilles Dowek. La indecidibilidad de la tipabilidad en el cálculo lambda-pi . En M. Bezem, JF Groote (Eds.), Cálculos lambda tipados y aplicaciones. Volumen 664 de Lecture Notes in Computer Science , 139–145, 1993.
• David Pym. Demostraciones, búsqueda y computación en lógica general . Tesis doctoral, Universidad de Edimburgo, 1990.
• David Pym. Un algoritmo de unificación para la${\displaystyle \lambda \Pi }$-cálculo. Revista Internacional de Fundamentos de Ciencias de la Computación 3(3), 333–378, 1992.

• Marcos lógicos específicos e implementaciones (una lista mantenida por Frank Pfenning , pero en su mayoría enlaces rotos desde 1997).