Getting Saturated with Induction
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910348375752704 |
|---|---|
| author | Hajdu, Márton Hozzová, Petra Kovács, Laura Reger, Giles Voronkov, Andrei |
| author_facet | Hajdu, Márton Hozzová, Petra Kovács, Laura Reger, Giles Voronkov, Andrei |
| contents | Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of first-order theorem proving. We describe our induction inference rules proving properties with inductively defined datatypes and integers. We also present additional reasoning heuristics for strengthening inductive reasoning, as well as for using induction hypotheses and recursive function definitions for guiding induction. We present exhaustive experimental results demonstrating the practical impact of our approach as implemented within Vampire.
This is an extended version of a Principles of Systems Design 2022 paper with the same title and the same authors. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_18954 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Getting Saturated with Induction Hajdu, Márton Hozzová, Petra Kovács, Laura Reger, Giles Voronkov, Andrei Logic in Computer Science Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of first-order theorem proving. We describe our induction inference rules proving properties with inductively defined datatypes and integers. We also present additional reasoning heuristics for strengthening inductive reasoning, as well as for using induction hypotheses and recursive function definitions for guiding induction. We present exhaustive experimental results demonstrating the practical impact of our approach as implemented within Vampire. This is an extended version of a Principles of Systems Design 2022 paper with the same title and the same authors. |
| title | Getting Saturated with Induction |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2402.18954 |