Homepage of Kryštof Hoder
My work on the Vampire theorem prover
Unfortunatelly, I no longer work on Vampire.
If you are struggling with Vampire, and unofficial readme can be found here.
- 160,000 lines of code (14 March 2012)
- Atom equivalence detection using Simultaneous SAT sweeping
- Congruence closure algorithm
- SMTLIB1.2 parser
- Several preprocessing rules based on quantified AIGs
- Predicate definition inlining
- Proof localization
- Interpolant minimization using an external SMT solver
- Tabulation based proof search algorithm
- InstGen calculus
- Global subsumption resolution (using our proof-tracking SAT solver)
- Unit-resulting resolution
- Preprocessing rules for predicate definitions and preserving/restoring EPR in their presence
- API for formula manipulation and clausification
- Let...in and if-then-else constructs
- Participation on the CASC-J5 competition
The new version of Vampire (0.6) has won the FOF, CNF and LTB divisions.
- Limited multiprocessing support implemented for reasoning with large theories
- 100,000 lines of code reached! (29 June 2010)
- Evaluation of interpreted symbols
- Efficient work with large theories
- Forward subsumption and demodulation indexing based on code trees
- Various methods of clause splitting
- Colouring of signature symbols with retrieval of interpolants and output of consequences of symbol eliminating inferences
- Participation on the CASC-22 competition
In combination with an old version of Vampire it has won the FOF division, and (using the SInE axiom selection) also the LTB division.
- Use of binary decision diagrams and an incremental SAT solver to handle propositional predicates
- Discount, Otter and LRS saturation algorithm implementation
- Substitution tree index implementation
My other work
As part of the CASC travel prize, I have visited in February 2012 the Theorem Proving Group at TU Munich and gave four talks: Automated Theorem Proving and Vampire, Sine Axiom Selection, Interpolant Minimization with Proof Transformations and Fixed Points and the μZ Engine (parts of the slides are reused from my co-authors' presentations)
Co-organiser of the First-order theorem proving and Vampire tutorial, held as part of the CADE 2011 conference on August 1, 2011 in Wroclaw, Poland. My slides on Vampire usage are here, examples used in the slides here.
SInE — axiom selection system, winner of the CASC-J4 (and in some sense also CASC-22 and CASC-J5) LTB division.
Generalized property directed reachability, K. Hoder, N. Bjorner
Accepted to SAT 2012
Playing in the Grey Area of Proofs, K. Hoder, L. Kovacs, A. Voronkov
Case Studies on Invariant Generation Using a Saturation Theorem Prover, K. Hoder, L. Kovacs, A. Voronkov
Sine Qua Non for Large Theory Reasoning, K. Hoder, A. Voronkov
CADE 2011 (slides)
μZ — An Efficient Engine for Fixed-points with Constraints, K. Hoder, N. Bjorner, L. de Moura
CAV 2011 (my slides from Dagstuhl presentation)
Invariant Generation in Vampire, K. Hoder, L. Kovacs, A. Voronkov
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library, J. Urban, K. Hoder, A. Voronkov
Symbol Elimination and Interpolation in Vampire, K. Hoder, L. Kovacs, A. Voronkov
Comparing Unification Algorithms in First-Order Theorem Proving, K. Hoder, A. Voronkov