Homepage of Kryštof Hoder

I am a PhD student at the School of Computer Science of the University of Manchester, supervised by Andrei Voronkov. My resume can be downloaded here.

My work on the Vampire theorem prover

The Vampire theorem prover is available for download at vprover.org. Become fan of Vampire.

Planning to do

• New techniques for term indexing
• Support for commutative function symbols
• Multiprocessing support
• Further support for interpreted symbols

Work done

• 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

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.

Efficient Datalog engine extended with means to handle infinite domains. Implemented during internship in Microsoft Research as part of the Z3 SMT solver. (slides)

Unification index benchmarking — a framework for comparing unification indexes based on COMPIT.

SInE — axiom selection system, winner of the CASC-J4 (and in some sense also CASC-22 and CASC-J5) LTB division.

Publications  [DBLP]

• Playing in the Grey Area of Proofs, K. Hoder, L. Kovacs, A. Voronkov
  Accepted to POPL 2012
• Case Studies on Invariant Generation Using a Saturation Theorem Prover, K. Hoder, L. Kovacs, A. Voronkov
  Accepted to MICAI 2011
• 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
  TACAS 2011
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library, J. Urban, K. Hoder, A. Voronkov
  ICMS 2010
• Symbol Elimination and Interpolation in Vampire, K. Hoder, L. Kovacs, A. Voronkov
  IJCAR 2010
• Comparing Unification Algorithms in First-Order Theorem Proving, K. Hoder, A. Voronkov
  KI 2009

 

Contact

 

 
Google Profile