| 2024 | IJCAR | On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus. | Uwe Waldmann |
| 2024 | ITP | A Modular Formalization of Superposition in Isabelle/HOL. | Martin Desharnais, Balzs Tth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret |
| 2020 | CADE | A Comprehensive Framework for Saturation Theorem Proving. | Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette |
| 2019 | CADE | Superposition with Lambdas. | Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann |
| 2018 | CADE | Superposition for Lambda-Free Higher-Order Logic. | Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann |
| 2018 | CADE | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann |
| 2017 | CADE | A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. | Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
| 2017 | CADE | Towards Strong Higher-Order Automation for Fast Interactive Verification. | Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann |
| 2017 | FOSSACS | A Lambda-Free Higher-Order Recursive Path Order. | Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
| 2015 | CADE | Beagle - A Hierarchic Superposition Theorem Prover. | Peter Baumgartner, Joshua Bax, Uwe Waldmann |
| 2015 | TABLEAUX | Modal Tableau Systems with Blocking and Congruence Closure. | Renate A. Schmidt, Uwe Waldmann |
| 2014 | CADE | Finite Quantification in Hierarchic Theorem Proving. | Peter Baumgartner, Joshua Bax, Uwe Waldmann |
| 2014 | CADE | Hierarchic Superposition Revisited. | Uwe Waldmann |
| 2013 | CADE | Hierarchic Superposition with Weak Abstraction. | Peter Baumgartner, Uwe Waldmann |
| 2009 | CADE | Superposition and Model Evolution Combined. | Peter Baumgartner, Uwe Waldmann |
| 2007 | ATVA | Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space. | Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz |
| 2007 | LPAR | An Extension of the Knuth-Bendix Ordering with LPO-Like Properties. | Michel Ludwig, Uwe Waldmann |
| 2006 | ATVA | Automatic Verification of Hybrid Systems with Large Discrete State Space. | Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz |
| 2005 | TABLEAUX | Comparing Instance Generation Methods for Automated Reasoning. | Swen Jacobs, Uwe Waldmann |
| 2004 | CADE | Modular Proof Systems for Partial Functions with Weak Equality. | Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann |
| 2003 | CADE | Superposition Modulo a Shostak Theory. | Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann |
| 2001 | CADE | Superposition and Chaining for Totally Ordered Divisible Abelian Groups. | Uwe Waldmann |
| 1999 | LPAR | Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups. | Uwe Waldmann |
| 1998 | CADE | Superposition for Divisible Torsion-Free Abelian Groups. | Uwe Waldmann |
| 1996 | CADE | Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). | Harald Ganzinger, Uwe Waldmann |
| 1993 | LICS | Set Constraints are the Monadic Class | Leo Bachmair, Harald Ganzinger, Uwe Waldmann |