pendientes.txt

La entidad Categoria deberia ser debil de usuario
en ifer.jsp se usa el resuelveManager dentro de un ciclo para ver si el teorema esta resuelto o no, esto es ineficiente
Al darle a demostrar deben aparecer los teoremas (no los axiomas) clickeables para escojer cual se va a demostrar
Si un teorema no admite un metodo de demostracion debe la opcion estar inabilitada
Has un orderby por numero de teorema a la lista de teoremas en los queries que ordene 3.4, 3.4.a y 3.5 en ese orden
Los metateoremas se desbloquean cuando estan demostrados todos los teoremas que usa como hipotesis

Nuevos

Cambiar el diseño de base de datos y hacer la migracion
Hacer un plan de pruebas de flujo de navegacion y automatizar las misma usando selenium
Hacer documentos del nuevo diseño de base de datos
Estamos trabajando con un sistema de abreviacion en donde hace falta conocer cual es el metodo de demostracion usado
Sabiendo cual es el metodo de demostracion usado se construye el arbol agregando los nodos correspondientes se podra inferir?
Estudiando el arbol parcial de derivacion, se puede inferir el metodo? si es asi no hace falta un campo en la tabla
Del arbol de derivacion final se puede deducir cual es el metodo de demostracion?
Idear un sistema homogeneo de creacion del arbol, basado en herencia, para todos los metodos de demostracion
Arreglar inferencia de tipo para el teorema E.p == algo
Arreglar la automatic substitution cuando hay aplicaciones funcionales en los paratodo y existe
Utilizar el metateorema 2 del libro para partir de un lado cuando la igualdad = es de terminos
Agregar en Go Back que se borre el metodo oculto cuando se usa metodo directo de una igualdad de funciones
Arreglar el problema de que nodejs no puede procesar string en latex muy largos, por ejemplo el 
teorema 9.9 por metodo directo en el primer paso aplicando 3.52 en el consecuente arroja este error de una
Arreglar el metateorema del True para teoremas que no contengan T (listo)
Revisar el formulario de editar simbolo si carga los campos que estan en la base de datos
Modificar que los datos inferibles del simbolo como infijo o rightassociativity se carguen en el formulario 
de editar simbolo sin que esten guardados en la base de datos
Arreglar el orden en que se ordenan las variables libres y por ende el orden en que se abstraen las mismas para 
que se puedan reconocer cuando un teorema ya existe salvo el nombre de las variables en todos los casos
Se lanza una excepcion cuando se trata de editar un teorema siendo AdminTeoremas
Siempre que se hace click en el + de un teorema, se hace el ajax para cargar todos los metateoremas, es suficiente 
que el ajax se haga solo la primera vez (listo)
En initStatementController cuando generarHistorial aborta, al usuario le sale el mensaje de que el metodo de 
demostracion no aplica a ese enunciado. Se debe separar los abort que dispara generarHistorial de los abort 
de initStatementController
Si la ultima linea es c_{1} x_{113} (c_{1} x_{113} x_{113}) se unifica erroneamente con el teorema c_{1} x_{113} x_{113} 
y sustitucion [x_{113} := (c_{1} x_{113} x_{113})]
Cambiar la direccion de la segunda subprueba de un AI cuando consta de una sola linea, actualizarla incluyendo MT
Bilsma dice que E:{true}y:=2{y=z} viola Leibniz as an axiom porque queda y=3=>true=false que no es un axioma, 
lo que no se ha dado cuenta es que y en E es ligada asi que cuando hagas E[z:=y] la y de E se renombraria, 
recuerda poner este ejemplo en la redaccion como lo importante de que las tripletas liguen las variables del programa
dependiendo del metodo, el sitio que se hace clickeable de color azul en un teorema de la lista derecha debe cambiar
si es directo y partir de un lado debe ser las equivalencias centrales, si es transitividad o debil-fortale debe ser 
el operador transitivo central, si es asumir el antecedente debe ser recursivamente la regla anterior aplicada en 
los consecuentes si el antecedente es unificable con la hipotesis
puse en todos abstractEq(null) el null se tiene que reemplazar por Term[] el hash de tipos de las variables, pero para esto cada ecuacion debe tener seteado el tipo en su body()
Si el teorema anterior se inicia de la izquierda y se quiere reemplazar p por p\/p, se unifica con una letra griega rara
Cambiar en el parser de tipos que los tipos b y p son sinonimos y hazlo general para que cualquier caracter sea un tipo
En Term.g quita en la produccion de 'c' NUMBER '(' explist ') que se construye Const seteando los parametros de esInfijo, 
precedencia, asociatividad, etc
En TypedApp metodo type() para Leibniz se modifica el z del Leibniz, esto esta mal porque esa modificacion no debe ocurrir alli, sino afuera, ese metodo debe aplicar Leibniz sobre el E textual que indique la regla, esto debe ser asi para poder 
si se quiere usar un E especifico con cierto truco, la modificacion del z me cambiaria el truco que le meti al E. Luego de 
que cambies eso, ve para el finish de Generalizarion y modifica el Leibniz poniendo el E adecuado(no me decido sobre esto)
Los arboles que se han usado para los finish y para los metateoremas usan a lambda z. en los Leibniz, pero esta variable 
z puede chocar con los esquema de arboles que se diseñen, tienes que hacer un esquema de arboles que cambie esta variable 
de ser necesaria (se puso un z negativo para que nunca choque con las variables del usuario que son positivas)
En toStringFormatC tambien tienes que chequear el tipo para saber si en una igualdad imprimes equivalencia o igualdad
En toStringFormatC hay un if que si el operador raiz es variable se debe chequear si usa la letra E, creo que esto ya no va
Cuando la prueba es Starting one Side y no ha terminado, el closingComment se imprime, deberia ser solo cuando resuelto
En la impresion de los hint se esta actualmente cableando z como el nombre de la variable de reemplazo,debe parametrizarse
Cuando se edita el numero de un teorema no se valida si el numero ya existe en otro resuelve de otro teorema del usuario

En el libro 
Marco teorico (for dummies)
semantica de lenguajes de programacion
Acomodar el algoritmo de inferencias de tipos en base a combinadores
Metodos de demostracion que se agregaron
Busqueda de demostraciones analogas
Ejecucion simbolica en base a la semantica definida simbolicamente
Computo guiado por demostraciones y enunciar aplicaciones
Combinadores paralelos (Combinaton)
Busquedas de demostraciones, estudio de optimizaciones usando combinadores paralelos
Desafios y tendencias futuras
Conclusiones
Di en el libro que cada metodo tiene su propio imprimir, crear inferencia base, retroceder, addInferToProof, interfazm y 
getLastLineOfProof

Para Baralt
Definiciones y axiomas para la aplicacion funcional a nivel sintactico
Definiciones y axiomas alternativos para la aplicacion funcional basado en combinadores (hacerlo para cualquier base de combinadores)
Definir la teoria de la funcionalidad, que es una teoria ecuacional de funciones
Dar la idea de lo que es logica de combinadores ilativa
Decir que no hace falta la logica de combinadores ilativa sino con la teoria ecuacional funcional pero considerando los conectores logicos y cuant
El resultado principal es que se tiene un algoritmo que es capaz de traducir inyectivamente cualquier prueba de la teoria de conjuntos ZF usando 
el sistema de deduccion natural, a una prueba en un fragmento ecuacional de la logica de Curry sin combinadores ilativos y sin esquema de axiomas. 
Por lo tanto, la validez de todo enunciado respecto a la consistencia de la teoria de conjuntos de Zermelo-Fraenkel, usando el sistema de deduccion 
natural, seria la misma en el fragmento de la logica de Curry antes mencionado
La traduccion se hace por medio de varias etapas: Primero se codifica una prueba usando el sistema de deduccion natural, en una prueba usando la 
logica de Dijkstra-Scholten, luego se explica una forma de codificar toda prueba de la logica de Dijkstra-Scholten en el sistema de conversion 
lambda (lambda-Calculo) de Church, por ultimo se explica una forma de codificar este fragmento de pruebas hechas con lambda-calculo en pruebas 
usando logica combinatoria.

Decir que se definio nuevamente el sistema de inferencia de Dijkstra-Scholten completando las ambiguedades que existen en la bibliografica, de 
forma que sea extrictamente formal y mecanizable

En el capitulo x se extiende la idea de la traduccion para ser usando en otras teorias distintas a la de conjuntos pero usando el sistema formal de 
Dijkstra-Scholten. Sin embargo el sistema de Dijkstra-Scholten requiere que los funcionales sean funciones totales, por lo que la parcialidad de 
las funciones debe interpretarse de una forma no convencional, por lo que la semantica de Dijkstra-Scholten no seria convencional. En este 
capitulo se explica dicha semantica. Se da un algoritmo de forma tal que convierte cualquier semantica convencional para teorias que se prentenden 
usar en un sistema de deduccion natural con funcionales parciales, en una semantica para la misma teoria pero destinada a ser usada en el 
sistema formal de inferencia de Dijkstra-Scholten.

En el ultimo capitulo se muestran varios teoremas de la teoria de conjuntos no estandar hechas con el nuevo sistema de Dijkstra-Scholten dpropuesto 
para mostrar que efectivamente se pueden hacer las derivaciones necesarias con el nuevo sistema sobre la teoria de conuntos no estandar. De estos 
teoremas se identifican cuales son demostrados en el fragmento intuicionista de Dijkstra-Scholten y cuales no. De aquellos que fueron demostrados 
intuicionistamente, se conjetura un algoritmo que para estos casos en especifico corresponde a un realizability para estos teoremas. Abriendo el 
camino para una nueva investigacion sobre realizabilities de la teoria de conjuntos no estandar usando el sistema de Dijkstra-Scholten 
intuicionistamente