En la lógica intuicionista , las fórmulas de Harrop , que llevan el nombre de Ronald Harrop , son la clase de fórmulas definidas inductivamente de la siguiente manera: [1] [2] [3]
- Las fórmulas atómicas son Harrop, incluida la falsedad (⊥);
- es Harrop proporcionado y están;
- es Harrop para cualquier fórmula bien formada ;
- es Harrop proporcionado es y es cualquier fórmula bien formada;
- es Harrop proporcionado es.
Al excluir la disyunción y la cuantificación existencial (excepto en el antecedente de implicación), se evitan los predicados no constructivos , lo que tiene beneficios para la implementación informática. Desde un punto de vista constructivista, las fórmulas de Harrop se "comportan bien". Por ejemplo, en la aritmética de Heyting , las fórmulas de Harrop satisfacen una equivalencia clásica que no suele satisfacerse en la lógica constructiva: [1]
Las fórmulas de Harrop fueron introducidas alrededor de 1956 por Ronald Harrop e independientemente por Helena Rasiowa . [2] Las variaciones del concepto fundamental se utilizan en diferentes ramas de la matemática constructiva y la programación lógica .
Fórmulas hereditarias de Harrop y programación lógica
Una definición más compleja de fórmulas hereditarias de Harrop se utiliza en la programación lógica como una generalización de las cláusulas de Horn y forma la base del lenguaje λProlog . Las fórmulas hereditarias de Harrop se definen en términos de dos (a veces tres) conjuntos recursivos de fórmulas. En una formulación: [4]
- Fórmulas atómicas rígidas, es decir, constantes o fórmulas , son Harrop hereditarios;
- ¿Se proporciona Harrop hereditario? y están;
- ¿Se proporciona Harrop hereditario? es;
- ¿Se proporciona Harrop hereditario? es rígidamente atómico, y es una fórmula G.
Las fórmulas G se definen como sigue: [4]
- Las fórmulas atómicas son fórmulas G , incluida la verdad (⊤);
- es una fórmula G proporcionada y están;
- es una fórmula G proporcionada y están;
- es una fórmula G proporcionada es;
- es una fórmula G proporcionada es;
- es una fórmula G proporcionada es y es Harrop hereditario.
Ver también
Referencias
- ↑ a b Dummett, Michael (2000). Elementos del intuicionismo (2ª ed.). Prensa de la Universidad de Oxford . pag. 227. ISBN 0-19-850524-8.
- ^ a b AS Troelstra, H. Schwichtenberg. Teoría básica de la prueba . Prensa de la Universidad de Cambridge . ISBN 0-521-77911-1.Mantenimiento de CS1: utiliza el parámetro de autores ( enlace )
- ^ Ronald Harrop (1956). "Sobre disyunciones y enunciados existenciales en sistemas lógicos intuicionistas". Mathematische Annalen . 132 (4): 347. doi : 10.1007 / BF01360048 .
- ^ a b Dov M. Gabbay, Christopher John Hogger, John Alan Robinson, Manual de lógica en inteligencia artificial y programación lógica: programación lógica , Oxford University Press , 1998, p 575, ISBN 0-19-853792-1