En lógica , un marco lógico proporciona un medio para definir (o presente) una lógica como una firma en un orden superior teoría tipo de tal manera que demostrabilidad de una fórmula en la lógica original se reduce a un tipo habitar problema en el tipo de estructura de 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 marco lógico de Edimburgo más conocido, LF . Varias herramientas de prueba más recientes como Isabelle se basan en esta idea. [1]A diferencia de la incrustación directa, el enfoque del marco lógico permite incrustar muchas lógicas en el mismo tipo de sistema. [3]
Descripción general
Un marco lógico se basa en un tratamiento general de la sintaxis, las reglas y las pruebas mediante un cálculo lambda de tipo 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:
- Una caracterización de la clase de lógicas de objetos a representar;
- Un metalenguaje apropiado;
- Una caracterización del mecanismo por 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 mecanografiados se normalizan fuertemente y Church-Rosser y la propiedad de estar bien mecanografiados es decidible . Sin embargo, la inferencia de tipos es indecidible.
Una lógica está representada en el marco lógico LF por 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 objeto se consideran pruebas primitivas de juicios hipotético-generales..
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 inductivo de teoremas meta-lógicos
Ver también
Referencias
- ↑ a b Bart Jacobs (2001). Lógica categórica y teoría de tipos . Elsevier. pag. 598. ISBN 978-0-444-50853-9.
- ^ Dov M. Gabbay, ed. (1994). ¿Qué es un sistema lógico? . Prensa de Clarendon . pag. 382. ISBN 978-0-19-853859-2.
- ^ Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Ingeniería del lenguaje y desarrollo de software riguroso (sic): International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, 24 de febrero - 1 de marzo de 2008, artículos seleccionados revisados . 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 fiabilidad del sistema (PDF) . Springer . 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 de cálculo lambda tipado para implementar sistemas formales en una máquina . Revista de razonamiento automatizado, 9: 309-354, 1992.
- Robert Harper. Una formulación ecológica 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 grupo-cálculo . Revista de lógica y computación 12 (6), 1061-1104, 2002.
- Por 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 . Studia Logica 54: 199-230, 1995.
- David Pym y Lincoln Wallen . Prueba de búsqueda en el-cálculo . En: G. Huet y G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.
- Didier Galmiche y David Pym. Búsqueda de pruebas en lenguajes teóricos de tipos: una introducción . Ciencias de la Computación Teórica 232 (2000) 5-53.
- Philippa Gardner. Representar la lógica 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 tipificabilidad en el cálculo lambda-pi . En M. Bezem, JF Groote (Eds.), Typed Lambda Calculi and Applications. Volumen 664 de Lecture Notes in Computer Science , 139-145, 1993.
- David Pym. Pruebas, búsqueda y cómputo en lógica general . Doctor. tesis, Universidad de Edimburgo, 1990.
- David Pym. Un algoritmo de unificación para-cálculo. Revista Internacional de Fundamentos de la Ciencia de la Computación 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 muertos desde 1997)