12 de febrero de 2009

Función de lista de secuentes en arboles de pruebas: ¿Alguien conoce algo así?

Buenas,

Este post es para preguntar si alguien conoce algo parecido a esto (dado que ya he buscado en varios lugares y preguntado y nadie me ha sabido responder que haya algo así... pero debería haberlo ¿no?)

La idea es, dado un sistema de tipos deterministico, i.e. si me das un secuente y una regla de tipado, te doy la conclusión determinísticamente (Para ponerlo más claro, piensen en un sistema de tipos de segundo orden, donde hay un y la regla me dice que lo puedo eliminar reemplazando la por algo, bueno, eso no sería determinístico ya que a la la puedo reemplazar por diferentes cosas, algo determinístico en cambio sería si la regla fuese una familia de reglas (una por cada posible)), bueno, entonces, dado un sistema de tipos determinístico, lo que quiero es algo parecido a una función que tome una lista de sequentes y devuelva un árbol de prueba completo. O sea, es como si la función tuviera un árbol de pruebas vacío, donde sólo están las reglas a aplicar y los sequentes que hay en los axiomas, y cuando toma la lista de secuentes, los acomoda en los espacios vacíos de las hojas del árbol (o sea, los toma como hipótesis).

¿Se entiende la idea? Definirlo formalmente no es muy difícil, de hecho ya lo tengo hecho, pero quería saber si alguien conocía que ya exista algo así (como para no redefinir lo que ya existe).

Ya he preguntado a varias personas y nadie me supo decir que haya algo así, pero bueno, si a alguien esta "función" le suena parecido a algo que conozcan, avisen.