Proof Reconstruction: Parsing Proofs
Automated theorem provers (ATP) and proof assistants are among the developed sub-areas on automated reasoning, despite their approaches being certainly opposite, many new developments combine both techniques allowing a sub-proof to be automated using an ATP from within a proof assistant. Acting as a...
- Autores:
-
Gómez-Londoño, Alejandro
- Tipo de recurso:
- Fecha de publicación:
- 2015
- Institución:
- Universidad EAFIT
- Repositorio:
- Repositorio EAFIT
- Idioma:
- eng
- OAI Identifier:
- oai:repository.eafit.edu.co:10784/5484
- Acceso en línea:
- http://hdl.handle.net/10784/5484
- Palabra clave:
- first-order logic
automatic theorem provers
- Rights
- License
- Acceso abierto
| Summary: | Automated theorem provers (ATP) and proof assistants are among the developed sub-areas on automated reasoning, despite their approaches being certainly opposite, many new developments combine both techniques allowing a sub-proof to be automated using an ATP from within a proof assistant. Acting as a bridge between proof assistants and ATP, these systems known as hammers tend to enhance the functionality of an existing proof assistant, adding ATP capabilities into the interactive logical reasoning process. Agda a well known dependently typed functional programming language that can also be use as a proof assistant lacks in some degree of a hammer-like tool, and hence our goal is to fill part of this gap with a tool that can translate from an ATP generated proof into idiomatic Agda code, and doing so provide a base for further development. |
|---|