Saturating Sorting without Sorts
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_ | 1866916148926218240 |
|---|---|
| author | Georgiou, Pamina Hajdu, Márton Kovács, Laura |
| author_facet | Georgiou, Pamina Hajdu, Márton Kovács, Laura |
| contents | We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures.
We formalize the semantics of recursive programs in many-sorted first-order logic and integrate sortedness/permutation properties within our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories, such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and hence concrete sorts. We formalize the permutation property of lists in first-order logic so that we automatically prove verification conditions of such algorithms purely by superpositon-based first-order reasoning. Doing so, we adjust recent efforts for automating inducion in saturation. We advocate a compositional approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. Our work turns saturation-based first-order theorem proving into an automated verification engine by (i) guiding automated inductive reasoning with manual proof splits and (ii) fully automating inductive reasoning in saturation. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_03712 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Saturating Sorting without Sorts Georgiou, Pamina Hajdu, Márton Kovács, Laura Logic in Computer Science Symbolic Computation We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted first-order logic and integrate sortedness/permutation properties within our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories, such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and hence concrete sorts. We formalize the permutation property of lists in first-order logic so that we automatically prove verification conditions of such algorithms purely by superpositon-based first-order reasoning. Doing so, we adjust recent efforts for automating inducion in saturation. We advocate a compositional approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. Our work turns saturation-based first-order theorem proving into an automated verification engine by (i) guiding automated inductive reasoning with manual proof splits and (ii) fully automating inductive reasoning in saturation. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort. |
| title | Saturating Sorting without Sorts |
| topic | Logic in Computer Science Symbolic Computation |
| url | https://arxiv.org/abs/2403.03712 |