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...

Full description

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
id REPOEAFIT2_05e1e9218dae71baced5c83c130cb2bc
oai_identifier_str oai:repository.eafit.edu.co:10784/5484
network_acronym_str REPOEAFIT2
network_name_str Repositorio EAFIT
repository_id_str
spelling 2015-06-29T21:03:16Z2015-06-102015-06-29T21:03:16Zhttp://hdl.handle.net/10784/5484Automated 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.engUniversidad EAFITGrupo de Investigación en Lógica y ComputaciónUniversidad EAFIT. Escuela de CienciasProof Reconstruction: Parsing ProofsworkingPaperinfo:eu-repo/semantics/workingPaperDocumento de trabajo de investigacióndrafthttp://purl.org/coar/version/c_b1a7d7d4d402bccehttp://purl.org/coar/resource_type/c_8042Acceso abiertohttp://purl.org/coar/access_right/c_abf2first-order logicautomatic theorem proversUniversidad EAFIT. Escuela de Ciencias. Grupo de Investigación en Lógica y ComputaciónGómez-Londoño, Alejandro (agomezl@eafit.edu.co)Gómez-Londoño, AlejandroLICENSElicense.txtlicense.txttext/plain; charset=utf-82556https://repository.eafit.edu.co/bitstreams/05353443-a69a-4541-a7d5-51a464434ab3/download76025f86b095439b7ac65b367055d40cMD51ORIGINALAlejandroGomezLondono_TechnicalReport.pdfAlejandroGomezLondono_TechnicalReport.pdfapplication/pdf194459https://repository.eafit.edu.co/bitstreams/ed3c5fdd-4063-4240-9db5-734154274d57/downloadd29b7e70eff03435e76e6eb13c421b8eMD5210784/5484oai:repository.eafit.edu.co:10784/54842015-06-29 17:09:48.117open.accesshttps://repository.eafit.edu.coRepositorio Institucional Universidad EAFITrepositorio@eafit.edu.co
dc.title.spa.fl_str_mv Proof Reconstruction: Parsing Proofs
title Proof Reconstruction: Parsing Proofs
spellingShingle Proof Reconstruction: Parsing Proofs
first-order logic
automatic theorem provers
title_short Proof Reconstruction: Parsing Proofs
title_full Proof Reconstruction: Parsing Proofs
title_fullStr Proof Reconstruction: Parsing Proofs
title_full_unstemmed Proof Reconstruction: Parsing Proofs
title_sort Proof Reconstruction: Parsing Proofs
dc.creator.fl_str_mv Gómez-Londoño, Alejandro
dc.contributor.department.spa.fl_str_mv Universidad EAFIT. Escuela de Ciencias. Grupo de Investigación en Lógica y Computación
dc.contributor.eafitauthor.spa.fl_str_mv Gómez-Londoño, Alejandro (agomezl@eafit.edu.co)
dc.contributor.author.none.fl_str_mv Gómez-Londoño, Alejandro
dc.subject.keyword.spa.fl_str_mv first-order logic
automatic theorem provers
topic first-order logic
automatic theorem provers
description 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.
publishDate 2015
dc.date.available.none.fl_str_mv 2015-06-29T21:03:16Z
dc.date.issued.none.fl_str_mv 2015-06-10
dc.date.accessioned.none.fl_str_mv 2015-06-29T21:03:16Z
dc.type.eng.fl_str_mv workingPaper
dc.type.none.fl_str_mv info:eu-repo/semantics/workingPaper
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_b1a7d7d4d402bcce
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_8042
dc.type.local.spa.fl_str_mv Documento de trabajo de investigación
dc.type.hasVersion.spa.fl_str_mv draft
dc.identifier.uri.none.fl_str_mv http://hdl.handle.net/10784/5484
url http://hdl.handle.net/10784/5484
dc.language.iso.eng.fl_str_mv eng
language eng
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.local.spa.fl_str_mv Acceso abierto
rights_invalid_str_mv Acceso abierto
http://purl.org/coar/access_right/c_abf2
dc.publisher.spa.fl_str_mv Universidad EAFIT
dc.publisher.program.spa.fl_str_mv Grupo de Investigación en Lógica y Computación
dc.publisher.department.spa.fl_str_mv Universidad EAFIT. Escuela de Ciencias
institution Universidad EAFIT
bitstream.url.fl_str_mv https://repository.eafit.edu.co/bitstreams/05353443-a69a-4541-a7d5-51a464434ab3/download
https://repository.eafit.edu.co/bitstreams/ed3c5fdd-4063-4240-9db5-734154274d57/download
bitstream.checksum.fl_str_mv 76025f86b095439b7ac65b367055d40c
d29b7e70eff03435e76e6eb13c421b8e
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
repository.name.fl_str_mv Repositorio Institucional Universidad EAFIT
repository.mail.fl_str_mv repositorio@eafit.edu.co
_version_ 1814110265051971584

Publicaciones similares