Marco logico

En lógica , un marco lógico proporciona un medio para definir (o presentar) una lógica como una firma 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 tipo en el tipo marco. teoría. ^{[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 prueba más recientes como Isabelle se basan en esta idea. ^[1] A diferencia de una incrustación directa, el enfoque de marco lógico permite integrar muchas lógicas en el mismo sistema de tipos. ^[3]

Descripción general

Un marco lógico se basa en un tratamiento general de la sintaxis, reglas y pruebas mediante un cálculo lambda tipificado de forma dependiente . La sintaxis se trata en un estilo 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 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 = Lenguaje + Representación ".

LF

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 están relacionados por las proposiciones como principio de 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 clases de tipos, o familias de tipos). Es predicativo , todos los términos bien tipificados son fuertemente normalizantes y Church-Rosser y la propiedad de estar bien tipificados son decidibles . Sin embargo, la inferencia de tipos es indecidible.

Una lógica está representada en el marco lógico LF mediante el mecanismo de representación de juicios como tipos. Esto está inspirado en el desarrollo de Per Martin-Löf de la noción de juicio de Kant , en las Conferencias de Siena de 1983. Los dos juicios de orden superior, el hipotético y el general, corresponden al espacio funcional ordinario y dependiente, respectivamente. La metodología de los juicios como tipos es que los juicios se representan como los tipos de sus pruebas. Un sistema lógico está representado por su firma que asigna clases y tipos a un conjunto finito de constantes que representa 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 J\vdash K}$ ${\displaystyle \Lambda x\in J.K(x)}$ ${\displaystyle {\mathcal {L}}}$ ${\displaystyle \Lambda x\in C.J(x)\vdash K}$

El sistema Twelf de la Universidad Carnegie Mellon proporciona una implementación del marco lógico LF . Doce 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

Ver también

• Marco gramatical
• Torniquete (símbolo)

Referencias

1. Bart Jacobs (2001). Lógica categórica y teoría de tipos . Elsevier. pag. 598.ISBN​ 978-0-444-50853-9.
2. Dov M. Gabbay, ed. (1994). ¿Qué es un sistema lógico?. Prensa de Clarendon . pag. 382.ISBN​ 978-0-19-853859-2.
3. Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Ingeniería del lenguaje y desarrollo riguroso de software: Escuela de verano internacional LerNet ALFA 2008, Piriápolis, Uruguay, 24 de febrero - 1 de marzo de 2008, artículos revisados ​​y seleccionados. Saltador. pag. 48.ISBN​ 978-3-642-03152-6.

Otras lecturas

• 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 . Revista de la Asociación de Maquinaria de Computación, 40(1):143-184, 1993.
• Arnon Avron , Furio Honsell, Ian Mason y Randy Pollack. Uso del cálculo lambda tipificado para implementar sistemas formales en una máquina . Revista de razonamiento automatizado, 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 . Revista de Lógica y Computación 8, 809-838, 1998.
• Samin Ishtiaq y David Pym. Modelos de recursos de Kripke de un cálculo agrupado de tipo dependiente ${\displaystyle \lambda }$ . Revista de Lógica y Computación 12(6), 1061-1104, 2002.
• Según 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 prueba del cálculo ${\displaystyle \lambda \Pi }$ . Studia Lógica 54: 199-230, 1995.
• David Pym y Lincoln Wallen . Búsqueda de pruebas en el cálculo ${\displaystyle \lambda \Pi }$ . En: G. Huet y G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.
• Didier Galmiche y David Pym. Búsqueda de pruebas en lenguajes de teoría de tipos: una introducción . Informática teórica 232 (2000) 5-53.
• Philippa Gardner. Representación de lógicas en teoría de tipos . Informe técnico, Universidad de Edimburgo, 1992. Informe LFCS ECS-LFCS-92-227.
• Gilles Dowek. "La indecidibilidad de la tipificación en el cálculo lambda-pi" . En M. Bezem, JF Groote (Eds.), Cálculos y aplicaciones Lambda mecanografiados. Volumen 664 de Lecture Notes in Computer Science , 139-145, 1993.
• David Pym. Pruebas, Búsqueda y Computación en Lógica General . Doctor. tesis, Universidad de Edimburgo, 1990.
• David Pym. Un algoritmo de unificación para el cálculo. ${\displaystyle \lambda \Pi }$ Revista internacional de fundamentos de la informática 3(3), 333-378, 1992.

enlaces externos

• Implementaciones y marcos lógicos específicos (una lista mantenida por Frank Pfenning , pero en su mayoría enlaces inactivos de 1997)