tstp2agda-0.1.0.0: Proof-term reconstruction from TSTP to Agda
- Author
- Alejandro Gómez-Londoño
- agomezl@eafit.edu.co
- Date
- December 19 2015
- Homepage
- https://github.com/agomezl/tstp2agda
- Documentation
- http://agomezl.github.io/doc/html/tstp2agda/index.html
- Issues
- https://github.com/agomezl/tstp2agda/issues
- Description
- A library for translating TSTP proofs into Agda code
To get started see the documentation for T2A module below
To date a number of restrictions and limitations are present
- Only proofs generated by the Metis 2.3 (release 20150303) ATP are supported
- Lack of complete first-order logic support, currently only propositional logic is supported
- Duplication errors with some proofs