Como discutimos en clase, cuando programamos en un lenguaje fuertemente tipificado debemos  
caracterizar mediante tipos el sistema que queremos construir.

Por ello definimos el tipo siguiente que nos permite construir proposiciones:

datatype Prop = lp of string | nega of Prop | conj of Prop * Prop | disy of Prop * Prop | impl of 
Prop * Prop;

Quedamos también que el sistema de Gentzen se basa en el concepto de secuente, y a su vez un secuente 
está conformado por dos secuencias de fórmulas, una izquierda (l) y una derecha (r).

Como en ML está interconstruido el tipo lista, podemos usar un alias (en este caso Sec de secuencia) 
para una lista de proposiciones, de la siguiente manera:

type Sec = Prop list;

Una vez que definimos secuencias podemos definir como construir secuentes mediante:

datatype Secuente = lr of Sec * Sec;

Posteriormente, debemos recordar que en el sistema Gentzen tenemos axiomas (Ax), y dos formas de 
reglas de inferencia, aquellas que dado un secuente obtenemos sólo un secuente (InRuUno, 
coloquialmente las que no bifurcan), y aquellas que dado un secuente obtenemos otros dos secuentes 
(InRuDos, coloquialmente las que bifurcan), lo cual podemos definir en ML mediante:

datatype SistemaG = Ax of Secuente | InRuUno of Secuente | InRuDos of Secuente * Secuente;

Después deben definir una función, digamos reduce, que tome un elemento de tipo Secuente y regrese 
un elemento de tipo SistemaG, esta función hace el trabajo de descomponer los conectivos tanto en la 
parte izquierda como en la derecha de un secuente, en notación de ML tendriamos:

val reduce = fn : Secuente -> SistemaG

Finalmente, deben definir una función que dado un elemento de SistemaG obtenga true o false, es 
decir, que pruebe si de la secuencia de fórmulas de la izquierda de un secuente se sigue la secuencia 
de fórmulas de la derecha del secuente, en terminología ML tendriamos:

val prueba = fn : SistemaG -> bool

Coloquialmente, la función reduce permite ir de un nodo a otro del árbol de prueba, y la 
función prueba construye el árbol de prueba completo.

Un ejemplo de prueba es:
Si queremos saber si es un tautología (o teorema) (p -> q) -> (~q -> ~p) debemos hacer lo siguiente 
en ML:

prueba(InRuUno(lr([],[impl(impl(lp("p"),lp("q")),impl(nega(lp("q")),nega(lp("p"))))])));

a lo que debe responder con:

val it = true : bool

Notas:
1 Obviamente habrá que escribir algunas funciones auxiliares,
2 Los elementos de SistemaG construidos con Ax se mapean a true si la parte izquierda y derecha de 
su secuente intersectan,
3 Los elementos de SistemaG construidos con InRuUno se mapean a true si recursivamente la reducción 
de su secuente se mapea a true,
4 Los elementos de SistemaG construidos con InRuDos se mapean a true si recursivamente la reducción 
de sus dos secuentes se mapean a true.

¡Disfrútenlo!