Lógica mínima

Sistema de lógica simbólica

La lógica mínima , o cálculo mínimo , es un sistema de lógica simbólica desarrollado originalmente por Ingebrigt Johansson . ^[1] Es una lógica intuicionista y paraconsistente , que rechaza tanto la ley del tercero excluido como el principio de explosión ( ex falso quodlibet ), y por tanto no mantiene como válida ninguna de las dos derivaciones siguientes:

${\displaystyle \vdash (B\lor \neg B)}$

${\displaystyle (A\land \neg A)\vdash }$

donde y son proposiciones cualesquiera. La mayoría de las lógicas constructivas sólo rechazan la primera, la ley del tercio excluido. En la lógica clásica, las leyes ex falso ${\displaystyle A}$ ${\displaystyle B}$

${\displaystyle (A\land \neg A)\to B,}$

${\displaystyle \neg (A\lor \neg A)\to B,}$

${\displaystyle \neg A\to (A\to B),}$

así como sus variantes con y switched, son equivalentes entre sí y válidos. La lógica mínima también rechaza esos principios. ${\displaystyle A}$ ${\displaystyle \neg A}$

Téngase en cuenta que el nombre a veces también se ha utilizado para designar sistemas lógicos con un número restringido de conectores.

Axiomatización

La lógica mínima se axiomatiza sobre el fragmento positivo de la lógica intuicionista. Ambas lógicas pueden formularse en el lenguaje utilizando los mismos axiomas de implicación , conjunción y disyunción que los conectivos básicos , pero la lógica mínima convencionalmente agrega el falsum o absurdo como parte del lenguaje. ${\displaystyle \to }$ ${\displaystyle \land }$ ${\displaystyle \lor }$ ${\displaystyle \bot }$

Son posibles otras formulaciones, siempre que se evite la explosión. A continuación se dan axiomas directos para la negación. Un desiderátum es siempre la ley de introducción de la negación, que se analiza a continuación.

Teoremas

Introducción de la negación

Un rápido análisis de las reglas válidas para la negación da una buena idea de lo que esta lógica, a falta de una explosión total, puede y no puede probar. Un enunciado natural en un lenguaje con negación , como la lógica mínima, es, por ejemplo, el principio de introducción de la negación , por el cual la negación de un enunciado se prueba suponiendo el enunciado y derivando una contradicción. Sobre la lógica mínima, el principio es equivalente a

${\displaystyle (B\to (A\land \neg A))\to \neg B}$,

Para dos proposiciones cualesquiera. Porque, tomada como la contradicción misma, esto establece la ley de no contradicción. ${\displaystyle B}$ ${\displaystyle A\land \neg A}$

${\displaystyle \neg (A\land \neg A)}$.

Suponiendo que cualquier , la regla de introducción del condicional material da , también cuando y no están relacionados de manera relevante . Con esto y la eliminación de implicación, el principio de introducción anterior implica ${\displaystyle C}$ ${\displaystyle B\to C}$ ${\displaystyle B}$ ${\displaystyle C}$

${\displaystyle (A\land \neg A)\to \neg B}$,

Es decir, suponiendo que exista alguna contradicción, toda proposición puede ser negada. La introducción de la negación es posible en la lógica minimal, por lo que aquí cualquier contradicción prueba además cualquier doble negación. La explosión permitiría eliminar esta última doble negación, pero este principio no se adopta. ${\displaystyle \neg \neg B}$

Axiomatización por vía del absurdo

Un posible esquema para extender el cálculo positivo a la lógica mínima es tratar como una implicación, en cuyo caso los teoremas del cálculo de implicación constructiva de una lógica se trasladan a los enunciados de negación. Para este fin, se introduce como una proposición, no demostrable a menos que el sistema sea inconsistente, y la negación se trata entonces como una abreviatura de . De manera constructiva, representa una proposición para la cual no puede haber ninguna razón para creerla. ${\displaystyle \neg B}$ ${\displaystyle \bot }$ ${\displaystyle \neg B}$ ${\displaystyle B\to \bot }$ ${\displaystyle \bot }$

Lo que sigue son argumentos rápidos que muestran qué teoremas todavía se mantienen en esta teoría lógica, a menudo haciendo uso implícito de la regla de curry válida y del teorema de deducción .

Trascendencia

Por introducción implícita, , y esto también implica mostrar directamente cómo suponer en lógica mínima prueba todas las negaciones. Puede expresarse como ${\displaystyle C\to (B\to C)}$ ${\displaystyle \bot \to (B\to \bot )}$ ${\displaystyle \bot }$

${\displaystyle \bot \to \neg B.}$

Si el absurdo es primitivo, el principio de explosión total también podría enunciarse como . ${\displaystyle \bot \to B}$

En cuanto a los principios adoptados en el cálculo de implicancias, que no implican negaciones, la página sobre el sistema de Hilbert los presenta a través de formas proposicionales de los axiomas de la ley de identidad , introducción de implicancias y una variante del modus ponens . Nótese la equivalencia demostrada allí. Para una primera derivación, al establecer aquí se obtiene inmediatamente el esquema ${\displaystyle {\big (}A\to (B\to C){\big )}\leftrightarrow {\big (}B\to (A\to C){\big )}}$ ${\displaystyle C=\bot }$

${\displaystyle {\big (}A\to \neg B{\big )}\leftrightarrow {\big (}B\to \neg A{\big )}}$.

En el sistema intuicionista de Hilbert, cuando no se introduce como una constante, esto puede tomarse como el segundo axioma que caracteriza la negación (el otro es la explosión). ${\displaystyle \bot }$

Ahora, en primer lugar, con tomado como , lo anterior demuestra que ${\displaystyle A}$ ${\displaystyle \neg B}$

${\displaystyle B\to \neg \neg B}$.

Pero, en segundo lugar, esta breve implicación también puede derivarse más directamente del modus ponens en la forma proposicional considerando . ${\displaystyle B\to ((B\to C)\to C)}$ ${\displaystyle C=\bot }$

En tercer lugar, de la forma débil válida de consequentia mirabilis se sigue : . En palabras, este teorema establece que un enunciado no puede rechazarse exactamente cuando la negación del enunciado implica que no puede rechazarse. En particular, se puede demostrar, por ejemplo, demostrando . ${\displaystyle (\neg B\to \neg \neg B)\leftrightarrow \neg \neg B}$ ${\displaystyle \neg \neg B}$ ${\displaystyle \neg B\to B}$

En cuarto lugar, la implicación de doble negación anterior también se sigue de

${\displaystyle {\big (}\neg \neg (A\to B){\big )}\to {\big (}A\to \neg \neg B{\big )}}$

que está relacionado con el principio de doble negación. Este teorema se puede establecer a partir de , razonando nuevamente con otra variable muy similar a la anterior, demostrando , y así sucesivamente. ${\displaystyle A\to {\big (}B\leftrightarrow (A\to B){\big )}}$ ${\displaystyle C}$ ${\displaystyle A\to {\big (}(\neg B)\leftrightarrow \neg (A\to B){\big )}}$

Contraposición de da ${\displaystyle B\to \neg \neg B}$

${\displaystyle \neg \neg \neg B\leftrightarrow \neg B}$.

Volviendo a uno de los teoremas anteriores, este también puede verse como un caso especial de con, nuevamente, . De hecho, el general puede derivarse del general . Alternativamente, lo mismo se sigue de , todo derivable de lo que se ha señalado anteriormente. Bajo la correspondencia Curry-Howard , el último teorema aquí también puede justificarse por la expresión lambda , solo por nombrar un ejemplo. ${\displaystyle {\big (}A\to \neg B{\big )}\leftrightarrow {\big (}\neg \neg A\to \neg B{\big )}}$ ${\displaystyle A=\neg B}$ ${\displaystyle {\big (}[(B\to C)\to C]\to C{\big )}\leftrightarrow (B\to C)}$ ${\displaystyle {\big (}A\to (B\to C){\big )}\leftrightarrow {\big (}([A\to C]\to C)\to (B\to C){\big )}}$ ${\displaystyle {\big (}[(B\to C)\to C]\to D{\big )}\to (B\to D)}$ ${\displaystyle \lambda f^{((B\to C)\to C)\to D}.\ \lambda b^{B}.\ f(\lambda g^{B\to C}.g(b))}$

Conjunciones

Yendo más allá de los enunciados únicamente en términos de implicaciones, los principios discutidos anteriormente ahora también pueden establecerse como teoremas: Con la definición de negación a través de , el enunciado modus ponens en la forma misma se especializa en el principio de no contradicción , al considerar . Cuando la negación es una implicación, entonces la forma currificada de no contradicción es nuevamente . Además, la introducción de la negación en la forma con una conjunción, explicada en la sección anterior, está implícita como el mero caso especial de ${\displaystyle \bot }$ ${\displaystyle (A\land (A\to C))\to C}$ ${\displaystyle C=\bot }$ ${\displaystyle A\to \neg \neg A}$ ${\displaystyle {\big (}B\to (A\land (A\to C)){\big )}\to (B\to C)}$

De esta manera, la lógica mínima puede caracterizarse como una lógica constructiva pero sin eliminación de la negación (también conocida como explosión).

Con esto se pueden obtener la mayoría de las implicaciones intuicionistas comunes que involucran conjunciones de dos proposiciones , incluida la equivalencia de curry.

Disyunciones

Vale la pena destacar la importante equivalencia

${\displaystyle {\big (}(A\lor B)\to C{\big )}\leftrightarrow {\big (}(A\to C)\land (B\to C){\big )}}$,

expresando que son dos formas equivalentes de decir que tanto y implican . De ello se obtienen dos de las conocidas leyes de De Morgan , ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle C}$

${\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B)}$.

También se puede derivar la tercera ley de De Morgan válida.

La negación de una afirmación de tercero excluido implica su propia validez. Con referencia a la variante débil de la consequentia mirabilis antes mencionada, se sigue que

${\displaystyle \neg \neg (B\lor \neg B)}$

Este resultado también puede verse como un caso especial de , que se deduce de cuando se considera para . ${\displaystyle {\big (}(B\lor (B\to C))\to C{\big )}\to C}$ ${\displaystyle ((A\lor B)\to C)\to (B\to C)}$ ${\displaystyle B\to C}$ ${\displaystyle A}$

Finalmente, el análisis de casos muestra

${\displaystyle {\big (}(B\lor \neg A)\land \neg \neg A{\big )}\to {\big (}(B\lor \neg B)\land \neg \neg B){\big )}}$

Esta implicación debe compararse con el silogismo disyuntivo completo , que se analiza en detalle más adelante.

Axiomatización mediante principios alternativos

Cabe señalar otro teorema que sólo implica implicaciones: relacionado con el principio de introducción de la negación, de

${\displaystyle (B\to A)\to ((A\to C)\to (B\to C))}$.

La lógica mínima demuestra la contraposición

${\displaystyle (B\to A)\to (\neg A\to \neg B)}$,

Lo cual, como la introducción de la negación, demuestra nuevamente que todos los principios anteriores se pueden obtener utilizando teoremas del cálculo positivo en combinación con la constante . ${\displaystyle (A\land \neg A)\to \neg B}$ ${\displaystyle \bot }$

En lugar de la formulación con esa constante, se puede adoptar como axioma el principio de contraposición que acabamos de enunciar, junto con el principio de doble negación . Esto da una axiomatización alternativa de la lógica minimal sobre el fragmento positivo de la lógica intuicionista. ${\displaystyle B\to \neg \neg B}$

Relación con la lógica clásica

La táctica de generalizar a no funciona para probar todas las afirmaciones clásicamente válidas que implican dobles negaciones. En particular, como era de esperar, la generalización ingenua de la eliminación de la doble negación no se puede probar de esta manera. De hecho, sea cual sea su aspecto, cualquier esquema de la forma sintáctica sería demasiado fuerte: considerar cualquier proposición verdadera para hace que esto sea equivalente a simplemente . ${\displaystyle \neg A}$ ${\displaystyle A\to C}$ ${\displaystyle \neg \neg B\to B}$ ${\displaystyle A}$ ${\displaystyle (A\to C)\to B}$ ${\displaystyle C}$ ${\displaystyle B}$

La proposición es un teorema de lógica mínima, tal como es . Por lo tanto, adoptar el principio de doble negación completo en la lógica mínima en realidad también prueba la explosión, y así lleva el cálculo de nuevo a la lógica clásica , saltándose también todas las lógicas intermedias . ${\displaystyle \neg \neg (B\lor \neg B)}$ ${\displaystyle (A\land \neg A)\to \neg \neg B}$ ${\displaystyle \neg \neg B\to B}$

Como se ha visto anteriormente, la doble negación del tercero excluido para cualquier proposición ya es demostrable en lógica minimal. Sin embargo, vale la pena enfatizar que en el cálculo de predicados, ni siquiera las leyes de la lógica intuicionista estrictamente más fuerte permiten una demostración de la doble negación de una conjunción infinita de enunciados de tercero excluido. De hecho,

${\displaystyle \nvdash \neg \neg \forall (n\in {\mathbb {N} }).Q(n)\lor \neg Q(n)}$

A su vez, el esquema de doble desplazamiento de negación (DNS) tampoco es válido, es decir

${\displaystyle \nvdash {\big (}\forall (n\in {\mathbb {N} }).\neg \neg P(n){\big )}\to \neg \neg \forall (n\in {\mathbb {N} }).P(n)}$

Más allá de la aritmética , esta imposibilidad de demostrarlo permite la axiomatización de teorías no clásicas.

Relación con la lógica paraconsistente

La lógica mínima demuestra variantes más débiles de la consequentia mirabilis , como se demuestra en ese artículo. Sin embargo, el principio completo es equivalente al tercio excluido.

Relación con la lógica intuicionista

Cualquier fórmula que utilice sólo es demostrable en lógica mínima si y sólo si es demostrable en lógica intuicionista. Pero también hay enunciados de lógica proposicional que no son demostrables en lógica mínima, pero que se cumplen en lógica intuicionista. ${\displaystyle \land ,\lor ,\to }$

El principio de explosión es válido en la lógica intuicionista y expresa que para derivar todas y cada una de las proposiciones, se puede hacerlo derivando cualquier absurdo. En la lógica mínima, este principio no se cumple axiomáticamente para proposiciones arbitrarias. Como la lógica mínima representa solo el fragmento positivo de la lógica intuicionista, es un subsistema de la lógica intuicionista y es estrictamente más débil.

En el caso de la explosión para las proposiciones negadas, la explosión completa es equivalente a su caso especial . Este último puede expresarse como eliminación de la doble negación para las proposiciones rechazadas, . Formulado de manera concisa, la explosión en la lógica intuicionista otorga exactamente casos particulares del principio de eliminación de la doble negación que la lógica mínima no tiene. Este principio también prueba inmediatamente el silogismo disyuntivo completo. ${\displaystyle ((\neg B)\land \neg (\neg B))\to B}$ ${\displaystyle \neg B\to (\neg \neg B\to B)}$

Silogismo disyuntivo

Prácticamente, en el contexto intuicionista, el principio de explosión posibilita el silogismo disyuntivo:

${\displaystyle ((A\lor B)\land \neg A)\to B.}$

Esto puede leerse de la siguiente manera: dada una prueba constructiva de y un rechazo constructivo de , se permite incondicionalmente la elección del caso positivo de . De esta manera, el silogismo es un principio de desempaquetamiento para la disyunción. Puede verse como una consecuencia formal de la explosión y también la implica. Esto se debe a que si se demostró probando entonces ya está probado, mientras que si se demostró probando , entonces también se sigue, ya que el sistema intuicionista permite la explosión. ${\displaystyle A\lor B}$ ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle A\lor B}$ ${\displaystyle B}$ ${\displaystyle B}$ ${\displaystyle A\lor B}$ ${\displaystyle A}$ ${\displaystyle B}$

Por ejemplo, dado un argumento constructivo de que el lanzamiento de una moneda dio como resultado cara o cruz ( o ), junto con un argumento constructivo de que el resultado en realidad no fue cara, el silogismo expresa que entonces esto ya constituye un argumento de que salió cruz. ${\displaystyle A}$ ${\displaystyle B}$

Si se supone metalógicamente que el sistema lógico intuicionista es consistente, el silogismo puede leerse como si dijera que una demostración constructiva de y , en ausencia de otros axiomas no lógicos que demuestren , en realidad contiene una demostración de . ${\displaystyle A\lor B}$ ${\displaystyle \neg A}$ ${\displaystyle B}$ ${\displaystyle B}$

En lógica mínima, no se puede obtener una prueba de de esta manera. Sin embargo, la misma premisa implica la doble negación de , es decir . Si se supone metalógicamente que el sistema de lógica mínima es consistente, entonces esa fórmula de implicación se puede expresar diciendo que simplemente no se puede rechazar. ${\displaystyle B}$ ${\displaystyle B}$ ${\displaystyle \neg \neg B}$ ${\displaystyle B}$

Las formas débiles de explosión prueban el silogismo disyuntivo y en la otra dirección, la instancia del silogismo con se lee y es equivalente a la eliminación de la doble negación para proposiciones para las que se cumple el término medio excluido. ${\displaystyle A=\neg B}$ ${\displaystyle {\big (}(B\lor \neg B)\land \neg \neg B{\big )}\to B}$

${\displaystyle (B\lor \neg B)\to (\neg \neg B\to B)}$.

Como el condicional material garantiza la eliminación de la doble negación para las proposiciones probadas, esto es a su vez equivalente a la eliminación de la doble negación para las proposiciones rechazadas.

Ejemplo intuicionista de uso en una teoría

El siguiente teorema aritmético de Heyting permite demostrar afirmaciones de existencia que no pueden demostrarse, mediante este resultado general, sin el principio de explosión. El resultado es esencialmente una familia de afirmaciones simples de eliminación de doble negación, oraciones que vinculan un predicado computable. ${\displaystyle \exists }$

Sea cualquier predicado libre de cuantificadores y, por tanto, decidible para todos los números , de modo que se cumpla el punto medio excluido, ${\displaystyle P}$ ${\displaystyle n}$

${\displaystyle P(n)\lor \neg P(n)}$.

Luego por inducción en , ${\displaystyle m}$

${\displaystyle \forall m.\ \neg {\big (}\forall (n<m).\neg P(n){\big )}\to \exists (b<m).P(b)}$

En palabras: Para los números dentro de un rango finito hasta , si se puede descartar que ningún caso es válido, es decir, si se puede descartar que para cada número, digamos , la proposición correspondiente siempre será refutable, entonces esto implica que hay alguno entre aquellos para los cuales es demostrable. ${\displaystyle n}$ ${\displaystyle m}$ ${\displaystyle n=a}$ ${\displaystyle P(a)}$ ${\displaystyle n=b}$ ${\displaystyle n}$ ${\displaystyle P(b)}$

Al igual que en los ejemplos analizados anteriormente, una prueba de esto requiere una explosión en el lado antecedente para obtener proposiciones sin negaciones. Si la proposición se formula como comenzando en , entonces este caso inicial ya da una forma de explosión a partir de una cláusula vacía ${\displaystyle m=0}$

${\displaystyle \bot \to \exists (b<0).P(b)}$.

El siguiente caso establece la eliminación de la doble negación para un predicado decidible, ${\displaystyle m=1}$

${\displaystyle \neg \neg P(0)\to P(0)}$.

El caso dice: ${\displaystyle m=2}$

${\displaystyle \neg {\big (}\neg P(0)\land \neg P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}}$,

lo cual, como ya se ha señalado, es equivalente a

${\displaystyle \neg \neg {\big (}P(0)\lor P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}}$.

Tanto y como son nuevamente casos de eliminación de la doble negación para un predicado decidible. Por supuesto, una afirmación para y fija puede ser demostrable por otros medios, utilizando principios de lógica mínima. ${\displaystyle m=0}$ ${\displaystyle m=1}$ ${\displaystyle \exists (b<m).P(b)}$ ${\displaystyle m}$ ${\displaystyle P}$

Por cierto, el esquema ilimitado para predicados decidibles generales ni siquiera es demostrable intuicionistamente; véase el principio de Markov .

Relación con la teoría de tipos

Uso de la negación

El absurdo se utiliza no sólo en la deducción natural , sino también en formulaciones teóricas de tipos según la correspondencia Curry-Howard . En los sistemas de tipos, también se suele introducir como tipo vacío. ${\displaystyle \bot }$ ${\displaystyle \bot }$

En muchos contextos, no es necesario que sea una constante independiente en la lógica, pero su función puede sustituirse por cualquier proposición rechazada. Por ejemplo, puede definirse como donde debe ser distinto. La afirmación de que no existe una prueba para esa proposición es entonces una afirmación de coherencia. ${\displaystyle \bot }$ ${\displaystyle a=b}$ ${\displaystyle a,b}$

Un ejemplo de caracterización de se encuentra en una teoría que involucra números naturales. Esto también puede adoptarse en lógica constructiva simple. Con esto, demostrar que es falso, es decir , solo significa demostrar que . También podemos introducir la notación para capturar la afirmación. Y, de hecho, usando aritmética, se cumple, pero también implica . Por lo tanto, esto implicaría y, por lo tanto, obtenemos . QED. ${\displaystyle \bot }$ ${\displaystyle 0=1}$ ${\displaystyle 3^{4}=8}$ ${\displaystyle \neg (3^{4}=8)}$ ${\displaystyle (3^{4}=8)\to (0=1)}$ ${\displaystyle 3^{4}\neq 8}$ ${\displaystyle {\tfrac {3^{4}-8}{73}}=1}$ ${\displaystyle (3^{4}=8)}$ ${\displaystyle {\tfrac {3^{4}-8}{73}}=0}$ ${\displaystyle 1=0}$ ${\displaystyle \neg (3^{4}=8)}$

Tipos simples

Los cálculos de programación funcional dependen en gran medida de la implicación conectiva, véase por ejemplo el cálculo de construcciones para un marco de lógica de predicados .

En esta sección mencionamos el sistema obtenido al restringir la lógica mínima a la implicación únicamente y lo describimos formalmente. Puede definirse mediante las siguientes reglas :

${\displaystyle {\dfrac {}{\Gamma \cup \{A\}\vdash A}}{\mbox{ axiom}}}$         ${\displaystyle {\dfrac {\Gamma \cup \{A\}\vdash B}{\Gamma \vdash A\to B}}{\mbox{ intro}}}$         ${\displaystyle {\dfrac {\Gamma \vdash A\to B~~~~~~~~~~\Delta \vdash A}{\Gamma \cup \Delta \vdash B}}{\mbox{ elim.}}}$^{[2] [3]}

Cada fórmula de esta lógica mínima restringida corresponde a un tipo en el cálculo lambda de tipos simples , véase la correspondencia de Curry-Howard . En ese contexto, la frase lógica mínima se utiliza a veces para referirse a esta restricción de la lógica mínima. ^[4] Este fragmento implicacional de la lógica mínima es el mismo que el fragmento implicacional positivo de la lógica intuicionista, ya que la lógica mínima ya es simplemente el fragmento positivo de la lógica intuicionista.

Semántica

Existen semánticas de lógica mínima que reflejan la semántica de marco de la lógica intuicionista (véase el análisis de la semántica en lógica paraconsistente) . En este caso, las funciones de valoración que asignan verdad y falsedad a las proposiciones pueden estar sujetas a menos restricciones.

Véase también

• Lógica intuicionista
• Lógica paraconsistente
• Cálculo proposicional implicacional
• Lista de sistemas lógicos

Notas

1. Johansson 1937.
2. Weber, Simons y Lafontaine 1993, págs. 36–40.
3. Huet 1986, págs. 125, 132.
4. Sørensen y Urzyczyn 1998.

Referencias

• Colacito, Almudena (2016). Lógica mínima y submínima de la negación (PDF) . Tesis de maestría (Afstudeerscriptie). Instituto de Lógica, Lenguaje y Computación .
• Huet, Gérard (mayo de 1986). Estructuras formales para computación y deducción. Escuela de verano internacional sobre lógica de programación y cálculos de diseño discreto. Archivado desde el original el 14 de julio de 2014.
• Johansson, Ingebrigt (1937). "Der Minimalkalkül, un reduzierter intuitionistischer Formalismus". Compositio Mathematica (en alemán). 4 : 119-136.
• Sørensen, Morten Heine B.; Urzyczyn, Paweł [en polaco] (mayo de 1998). "Conferencias sobre el isomorfismo de Curry-Howard" (PDF) .
• Troelstra, Anne Sjerp ; Schwichtenberg, Helmut (2003) [1996]. Teoría básica de la prueba (2 ed.). Prensa de la Universidad de Cambridge . págs. XII, 417. ISBN 9780521779111.
• Weber, Matthias; Simons, Martin; Lafontaine, Christine (1993). El lenguaje de desarrollo genérico Deva: presentación y estudios de casos . Apuntes de clase en informática (LNCS). Vol. 738. Springer. pág. 246. ISBN. 3-540-57335-6.