Lemmas: Generation, Selection, Application
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910297002868736 |
|---|---|
| author | Rawson, Michael Wernhard, Christoph Zombori, Zsolt Bibel, Wolfgang |
| author_facet | Rawson, Michael Wernhard, Christoph Zombori, Zsolt Bibel, Wolfgang |
| contents | Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2303_05854 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Lemmas: Generation, Selection, Application Rawson, Michael Wernhard, Christoph Zombori, Zsolt Bibel, Wolfgang Logic in Computer Science Artificial Intelligence Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search. |
| title | Lemmas: Generation, Selection, Application |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2303.05854 |