4 citations · 6 across the 4 of their papers we have counts for
4 papers
Partial Redundancy in Saturation
Márton Hajdu, Laura Kovács, Andrei Voronkov
Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We improve redundancy elimination by introducing a new notion of redundancy, ba…
Term Ordering Diagrams
Márton Hajdu, Robin Coutelier, Laura Kovács +1
The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO)…
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…
Getting Saturated with Induction
Márton Hajdu, Petra Hozzová, Laura Kovács +2
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 indu…