Omitir los comandos de cinta
Saltar al contenido principal
Inicio de sesión
Universidad EAFIT
Carrera 49 # 7 sur -50 Medellín Antioquia Colombia
Carrera 12 # 96-23, oficina 304 Bogotá Cundinamarca Colombia
(57)(4) 2619500 contacto@eafit.edu.co

Pregrado en Ingeniería Matemática/Prácticas investigativas Skip Navigation Linksciencias-computacion Ciencias de la computación

EAFITProgramasPregradosPregrado en Ingeniería MatemáticaPregrado en Ingeniería Matemática/Prácticas investigativasCiencias de la computación

Ciencias de la computación

2015-1

Proof Reconstruction: Parsing Proofs

Autor: Diego Alejandro Montoya Zapata.

Resumen:

The TPTP library has provided the community with standards for input and output for ATPs (Sutclie, 2009). However, it does not exist a standard for the way the proof is printed, which make it difficult to try to do a program to reconstruct the proofs for all of the ATPs. For this reason, we decided to focus our efforts in formulating the demonstration in Agda just for one ATP.