Daniel Wand

Doctoral researcher,


Max-Planck-Institut für Informatik
Saarland Informatics Campus E1 4
66123 Saarbrücken

+49 681 9325-2926, fax -2999



Physical address: building E1 5, room 621

My research focus on bridging the gap between high-order proof assistants and first-order automated theorem provers by extending the capabilities of the automated theorem provers to provide features usually found in proof assistants.

Academic Activities



    • Automating Induction inside Superposition
      Daniel Wand and Christoph Weidenbach.
      Draft   Syntax example file

    • Polymorphic Typed Superposition
      Daniel Wand and Christoph Weidenbach.


    • A lambda-free higher-order recursive path order
      Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. In Esparza, J., Murawski, A. S. (eds.) 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), LNCS 10203, pp. 461–479, Springer, 2017.
      PDF    Report

    • More SPASS with Isabelle — Superposition with hard sorts and configurable simplification
      Jasmin Cristian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach. In Beringer, L., Felty, A. P. (eds.) Third International Conference on Interactive Theorem Proving (ITP 2012), LNCS 7406, pp. 345–360, Springer, 2012.
      PDF    SPASS 3.8ds 32 bit linux-binary    SPASS 3.8ds 64 bit linux-binary    Sample file

    • Polymorphic+Typeclass Superposition
      Daniel Wand. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014).
      PDF    Web page    Syntax example file