1 citations · 3 across the 8 of their papers we have counts for
5 papers · 1 filter
Synthesis Benchmarks for Automated Reasoning
Márton Hajdu, Petra Hozzová, Laura Kovács +3
Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifica…
The Vampire Diary
Filip Bártek, Ahmed Bhayat, Robin Coutelier +10
During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now…
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)…
Positive Almost-Sure Termination of Polynomial Random Walks
Lorenz Winkler, Laura Kovács
The number of steps until termination of a probabilistic program is a random variable. Probabilistic program termination therefore requires qualitative analysis via almost-sure ter…