1 citations · 3 across the 7 of their papers we have counts for
Showing 2024Show all
2 papers · 1 filter
cs.LO2024
Saturating Sorting without Sorts
Pamina Georgiou, Márton Hajdu, Laura Kovács
We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formal…
cs.LO2024
Rewriting and Inductive Reasoning
Márton Hajdu, Laura Kovács, Michael Rawson
Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem…