VAMPIRE — PROGRAM
Days: Friday, 24 July 2026
Friday, 24 July 2026
Location:
C4.02
| 09:00-09:50 |
Vampire in Universal Algebra: Missing Tools [Invited talk] (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
|
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 |
Integrating Chronological and Graph Backtracking in AVATAR (abstract) 20 min
1 TU Wien
|
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
|
Location:
C4.02
| 15:30-15:50 |
Theorem Proving as Combinatorial Optimization: Toward Operations Research-Guided Strategy Design for Vampire (abstract) 20 min
1 Indiana University Bloomington
|
| 15:50-16:10 |
Exploiting Intra-Clausal Literal Sharing in Code Trees (abstract) 20 min
1 University of Bonn
|
| 16:10-16:30 |
Unification as a simple theorem prover (abstract) 20 min
1 None
|