6 papers
Completeness of Synthesis under Realizability Assumptions using Superposition
Márton Hajdu, Petra Hozzová, Laura Kovács +1
Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables t…
Lean on Vampire Proofs (Short Paper)
Jonas Bodingbauer, Márton Hajdu, Laura Kovács +2
Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampi…
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…
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…
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)…