Keyword:first-order theorem proving

Papers
Integrating Answer Literals with AVATAR for Program Synthesis Petra Hozzová In:Proceedings of the 7th and 8th Vampire Workshop
The Spawns of the Saturation Framework Sophie Tourret In:Proceedings of the 7th and 8th Vampire Workshop
Sorting Without Sorts Pamina Georgiou, Márton Hajdu and Laura Kovács EasyChair Preprint no. 10632
The Vampire Approach to Induction Márton Hajdu, Laura Kovács, Michael Rawson and Andrei Voronkov EasyChair Preprint no. 9217
Induction with Recursive Definitions in Superposition Márton Hajdu, Petra Hozzová, Laura Kovács and Andrei Voronkov EasyChair Preprint no. 6513
Integer Induction in Saturation Petra Hozzová, Laura Kovács and Andrei Voronkov EasyChair Preprint no. 5176
Induction with Generalization in Superposition Reasoning Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint no. 2468
Implementing Bottom-up Procedures with Code Trees: a Case Study of Forward Subsumption Andrei Voronkov EasyChair Preprint no. 3148
Aiming for the Goal with SInE Martin Suda In:Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
Experimenting with Theory Instantiation in Vampire Martin Riener In:Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny Sylvia Grewe, Sebastian Erdweg and Mira Mezini In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
The Challenges of Evaluating a New Feature in Vampire Giles Reger, Martin Suda and Andrei Voronkov In:Proceedings of the 1st and 2nd Vampire Workshops
Reasoning About Loops Using Vampire Laura Kovács and Simon Robillard In:Proceedings of the 1st and 2nd Vampire Workshops