More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. - Jasmin Christian Blanchette; Andrei Popescu 001; Daniel Wand; Christoph Weidenbach (ITP, 2012)

Polymorphic+Typeclass Superposition. - Daniel Wand (PAAR@IJCAR, 2014)

Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. - Heiko Becker; Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (Arch. Formal Proofs, 2016)

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. - Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (Arch. Formal Proofs, 2016)

A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. - Heiko Becker; Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (CADE, 2017)

A Lambda-Free Higher-Order Recursive Path Order. - Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand (FoSSaCS, 2017)

Superposition: Types and Induction. (Superposition : types et induction). - Daniel Wand (2017)