VAMPIRE — PROGRAM
Days: Friday, 24 July 2026
Friday, 24 July 2026
09:00-10:30
Equality reasoning(?)
Vampire
Location:
C4.02
| 09:00-09:50 |
Experimental Results for Vampire on the Equational Theories Project (abstract) 50 min
1 CTU, Prague
|
| 09:50-10:10 |
Some Experiments with Twee-Style Goal-Directedness (abstract) 20 min
1 DHBW Stuttgart
|
| 10:10-10:30 |
Reset Early, Reset Often, Eliminate Models (abstract) 20 min
1 University of Cambridge
|
10:30-11:00
Coffee Break
Vampire
Location:
C4.02
11:00-12:00
Machine learning
Vampire
Location:
C4.02
| 11:00-11:20 |
Machine-Learned Clause Selection: Intricacies and Surprises (abstract) 20 min
1 Czech Institute of Informatics, Robotics, and Cybernetics
|
| 11:20-11:40 |
ProofAtlas: A Saturation Prover with Integrated Neural Clause Selection (abstract) 20 min
1 TU Wien
|
| 11:40-12:00 |
Towards Lemma Mining: Concurrent Lemma Exploration via Vampire and Large Language Models (abstract) 20 min
1 Trinity College Dublin
|
12:00-13:40
Lunch
Vampire
Location:
C4.02
13:40-15:00
Proof checking & applications
Vampire
Location:
C4.02
| 13:40-14:00 |
VaLeaDATE: Checking TSTP Proofs for Soundness (abstract) 20 min
1 TU Wien
|
| 14:00-14:20 |
Lean on Thousands of Problems (abstract) 20 min
1 TU Wien
|
| 14:20-14:40 |
Identifying and Explaining (Non-)Equivalence of First-Order Logic Formulas (abstract) 20 min
1 Ruhr University Bochum
2 TU Dortmund University
3 Université Paris-Saclay, ENS Paris-Saclay
|
| 14:40-15:00 |
SigmaKEE-rs: An Embedded Ontological Reasoning System with Vampire as a Reusable Library Component (abstract) 20 min
1 Naval Postgraduate School
|
15:00-15:30
Coffee Break
Vampire
Location:
C4.02
15:30-16:50
Optimizations(?)
Vampire
Location:
C4.02
| 15:30-15:50 |
Integrating Chronological and Graph Backtracking in AVATAR (abstract) 20 min
1 TU Wien
|
| 15:50-16:10 |
Theorem Proving as Combinatorial Optimization: Toward Operations Research-Guided Strategy Design for Vampire (abstract) 20 min
1 Indiana University Bloomington
|
| 16:10-16:30 |
Exploiting Intra-Clausal Literal Sharing in Code Trees (abstract) 20 min
1 University of Bonn
|
| 16:30-16:50 |
Unification as a simple theorem prover (abstract) 20 min
1 None
|