Saturation-based theorem proving in higher-order and first-order logic.
A. Bentkamp, J. Blanchette, V. Nummelin, S. Tourret, P. Vukmirović, U. Waldmann:
Mechanical mathematicians,
in CACM, 66(4):80–90, 2023.
U. Waldmann, S. Tourret, S. Robillard, J. Blanchette:
A comprehensive framework for saturation theorem proving,
in JAR, 66:499–539, 2022.
A. Bentkamp, J. Blanchette, S. Cruanes, U. Waldmann:
Superposition for lambda-free higher-order logic,
in LMCS, 17(2):1–38, 2021.
A. Bentkamp, J. Blanchette, S. Tourret, P. Vukmirović, U. Waldmann:
Superposition with lambdas,
in JAR, 65:893–940, 2021.
A. Schlichtkrull, J. Blanchette, D. Traytel, U. Waldmann:
Formalizing Bachmair and Ganzinger's ordered resolution prover,
in JAR, 64:1169–1195, 2020.
U. Waldmann, S. Tourret, S. Robillard, J. Blanchette:
A comprehensive framework for saturation theorem proving,
in IJCAR 2020, LNAI 12166, pp. 316–334, 2020.
A. Bentkamp, J. C. Blanchette, S. Tourret, P. Vukmirović, U. Waldmann:
Superposition with lambdas,
in CADE 27, LNCS 11716, pp. 55–73, 2019.
A. Schlichtkrull, J. C. Blanchette, D. Traytel, U. Waldmann:
Formalizing of Bachmair and Ganzinger's ordered resolution prover,
in IJCAR 2018, LNCS 10900, pp. 89–107, 2018.
P. Baumgartner, U. Waldmann:
Hierarchic Superposition Revisited,
in Description Logic, Theory Combination, and All That, LNCS 11560, pp. 15–56, 2019.
A. Bentkamp, J. C. Blanchette, S. Cruanes, U. Waldmann:
Superposition for lambda-free higher-order logic,
in IJCAR 2018, LNAI 10900, pp. 28–46, 2018.
A. Schlichtkrull, J. C. Blanchette, D. Traytel, U. Waldmann:
Formalization of Bachmair and Ganzinger's ordered resolution prover,
in IJCAR 2018, LNAI 10900, pp. 89–107, 2018.
E. Althaus, et al.:
Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement,
in SCP, 148:123–160, 2017.
H. Becker, J. C. Blanchette, U. Waldmann, D. Wand:
A transfinite Knuth-Bendix order for lambda-free higher-order terms,
in CADE-26, LNAI 10395, pp. 432–453, 2017.
J. C. Blanchette, U. Waldmann, D. Wand:
A lambda-free higher-order recursive path order,
in FoSSaCS 2017, LNCS 10203, pp. 461–479, 2017.
R. A. Schmidt, U. Waldmann:
Modal Tableau Systems with Blocking and Congruence Closure,
in TABLEAUX 2015, LNAI 9323, pp. 38–53, 2015.
P. Baumgartner, J. Bax, U. Waldmann:
Beagle – A Hierarchic Superposition Theorem Prover,
in CADE-25, LNAI 9195, pp. 367–377, 2015.
U. Waldmann:
Hierarchic superposition revisited (Abstract),
invited talk, PAAR 2014.
P. Baumgartner, J. Bax, U. Waldmann:
Finite quantification in hierarchic theorem proving,
in IJCAR 2014, LNAI 8562, pp. 152–167, 2014.
P. Baumgartner, U. Waldmann:
Hierarchic superposition: Completeness without compactness,
in MACIS 2013, pp. 8–12, 2013.
P. Baumgartner, U. Waldmann:
Hierarchic superposition with weak abstraction,
in CADE-24, LNAI 7898, pp. 39–57, 2013.
T. Hillenbrand, R. Piskac, U. Waldmann, C. Weidenbach:
From search to computation: Redundancy criteria and simplification at work,
in Programming Logics, Essays in Memory of Harald Ganzinger, LNCS 7797, pp. 169–193, 2013.
W. Damm, et al.:
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces,
in SCP, 77(10–11):1122–1150, 2012.
P. Baumgartner, U. Waldmann:
A combined superposition and model evolution calculus,
in JAR, 47(2):191–227, 2011.
P. Baumgartner, U. Waldmann:
Superposition and model evolution combined,
in CADE-22, LNAI 5663, pp. 17–34, 2009.
W. Damm, et al.:
Exact state set representation in the verification of linear hybrid systems with large discrete state space,
in ATVA 2007, LNCS 4762, pp. 425–440, 2007.
M. Ludwig, U. Waldmann:
An extension of the Knuth-Bendix ordering with LPO-like properties,
in LPAR 2007, LNAI 4790, pp. 348–362, 2007.
S. Jacobs, U. Waldmann:
Comparing instance generation methods for automated reasoning,
in JAR, 38:57–78, 2007.
W. Damm, et al.:
Automatic verification of hybrid systems with large discrete state space,
in ATVA 2006, LNCS 4218, pp. 276–291, 2006.
H. Ganzinger, V. Sofronie-Stokkermans, U. Waldmann:
Modular proof systems for partial functions with Evans equality,
in I&C, 204:1453–1492, 2006.
V. Prevosto, U. Waldmann:
SPASS+T,
in ESCoR, pp. 18–33, 2006.
S. Jacobs, U. Waldmann:
Comparing instance generation methods for automated reasoning,
in TABLEAUX 2005, LNAI 3702, pp. 153–168, 2005.
H. Ganzinger, V. Sofronie-Stokkermans, U. Waldmann:
Modular proof systems for partial functions with weak equality,
in IJCAR 2004, LNAI 3097, pp. 168–182, 2004.
H. Ganzinger, T. Hillenbrand, U. Waldmann:
Superposition modulo a Shostak theory,
in CADE-19, LNAI 2741, pp. 182–196, 2003.
U. Waldmann:
Cancellative abelian monoids and related structures in refutational theorem proving (Part I).
in JSC, 33(6):777–829, 2002.
U. Waldmann:
Cancellative abelian monoids and related structures in refutational theorem proving (Part II).
in JSC, 33(6):831–861, 2002.
U. Waldmann:
A new input technique for accented letters in alphabetical scripts.
in IUC 20, 2002.
U. Waldmann:
Superposition and chaining for totally ordered divisible abelian groups.
in IJCAR 2001, LNAI 2083, pp. 226–241, 2001.
U. Waldmann:
Cancellative superposition decides the theory of divisible torsion-free abelian groups.
in LPAR'99, LNAI 1705, pp. 131–147, 1999.
U. Waldmann:
Extending reduction orderings to ACU-compatible reduction orderings.
in IPL, 67(1):43–49, 1998.
U. Waldmann:
Superposition for divisible torsion-free abelian groups.
in CADE-15, LNAI 1421, pp. 144–159, 1998.
U. Waldmann:
Cancellative Abelian Monoids in Refutational Theorem Proving.
PhD Thesis, Universität des Saarlandes, 1997.
H. Ganzinger, U. Waldmann:
Theorem proving in cancellative abelian monoids,
in CADE-13, LNAI 1104, pp. 388–402, 1996.
L. Bachmair, H. Ganzinger, U. Waldmann:
Refutational theorem proving for hierarchic first-order theories,
in AAECC, 5(3/4):193–212, 1994.
L. Bachmair, H. Ganzinger, U. Waldmann:
Superposition with simplification as a decision procedure for the monadic class with equality,
in KGC'93, LNCS 713, pp. 83–96, 1993.
L. Bachmair, H. Ganzinger, U. Waldmann:
Set constraints are the monadic class,
in LICS 8, pp. 75–83, 1993.
L. Bachmair, H. Ganzinger, U. Waldmann:
Theorem proving for hierarchic first-order theories,
in ALP'92, LNCS 632, pp. 420–434, 1992.
H. Ganzinger, U. Waldmann:
Termination proofs of well-moded logic programs via conditional rewrite systems,
in CTRS'92, LNCS 656, pp. 430–437, 1992.
U. Waldmann:
Semantics of order-sorted specifications.
in TCS, 94(1):1–35, 1992.
U. Waldmann:
Compatibility of order-sorted rewrite rules.
in CTRS'90, LNCS 516, pp. 407–416, 1990.
U. Waldmann:
Unitary unification in order-sorted signatures (extended abstract).
in UNIF'89, pp. 106–110, 1989.
U. Waldmann:
(Un)professional Publishing.
CADE-30,
30th International Conference on Automated Deduction,
Stuttgart, Germany, July 2025 (PC co-chair)
IJCAR 2024,
12th International Joint Conference on Automated Reasoning,
Nancy, France, July 2024 (PC member)
CADE-29,
29th International Conference on Automated Deduction,
Rome, Italy, July 2023 (PC member)
IJCAR 2022,
11th International Joint Conference on Automated Reasoning,
Haifa, Israel, August 2022 (PC member)
CADE-28,
28th International Conference on Automated Deduction,
Virtual Event, July 2021 (PC member)
IJCAR 2020,
10th International Joint Conference on Automated Reasoning,
Paris, France, July 2020 (PC member)
TABLEAUX 2019,
28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,
London, UK, September 2019 (PC member)
CADE-27,
27th International Conference on Automated Deduction,
Natal, Brazil, August 2019 (PC member)
DT 2018,
Deduktionstreffen,
Esch, Luxembourg, September 2018 (PC co-chair)
IJCAR 2018,
9th International Joint Conference on Automated Reasoning,
Oxford, UK, July 2018 (PC member)
IWIL 2017,
12th International Workshop on the Implementation of Logics,
Maun, Botswana, May 2017 (PC member)
PAAR-2016,
5th Workshop on Practical Aspects of Automated Reasoning,
Coimbra, Portugal, July 2nd, 2016 (PC member)
IWIL 2015,
11th International Workshop on the Implementation of Logics,
Suva, Fiji, November 2015 (PC member)
IJCAR 2014,
7th International Joint Conference on Automated Reasoning,
Vienna, Austria, July 2014 (PC member)
IWIL 2013,
10th International Workshop on the Implementation of Logics,
Stellenbosch, South Africa, December 2013 (PC member)
MACIS 2013,
Fifth International Conference on Mathematical Aspects of Computer
and Information Sciences,
Nanning, China, December 2013 (Track co-chair)
CADE-24,
24th International Conference on Automated Deduction,
Lake Placid, NY, USA, June 2013 (PC member)
LfSA'12,
CAV 2012 Workshop on Logics for System Analysis,
Berkeley, USA, July 2012 (PC member)
IWIL 2012,
LPAR-18 Workshop on the Implementation of Logics,
Merida, Venezuela, March 2012 (PC member)
LfSA'10,
FLoC 2010 Workshop on Logics for System Analysis,
Edinburgh, United Kingdom, July 2010 (PC member)
PAAR-2008,
IJCAR 2008 Workshop on Practical Aspects of Automated Reasoning,
Sydney, Australia, August 2008 (PC member)
ESARM,
CICM 2008 Workshop on Empirically Successful
Automated Reasoning for Mathematics,
Birmingham, United Kingdom, July/August 2008 (PC member)
ESARLT,
CADE-21 Workshop on Empirically Successful Automated Reasoning in Large
Theories,
Bremen, Germany, July 2007 (PC member)
ESCoR,
FLoC'06 Workshop on Empirically Successful Computerized Reasoning,
Seattle, USA, August 2006 (PC member)
RTA'03,
14th International Conference on Rewriting Techniques and Applications,
Valencia, Spain, June 2003 (PC member)
Mathematics in Computer Science, Special Focus on Constraints and Combinations, 9(3), 2015 (Guest editor, with Pascal Fontaine and Thomas Sturm)
AVACS - Automatic Verification and Analysis of Complex Systems (until December 2015)
Verisoft - Beweisen als Ingenieurwissenschaft (until June 2006)
PhD in Computer Science (Dr.-Ing.), Universität des Saarlandes, July 1997.
Thesis:
Cancellative
Abelian Monoids in Refutational Theorem Proving.
Diploma in Computer Science (Dipl.-Inf.), Universität Dortmund, August 1989.
Thesis: Vervollständigung von Spezifikationen mit Subsortendeklarationen
(Completion of Specifications with Subsort Declarations).
LICS Test-of-Time Award 2013 for Set constraints are the monadic class.
Winner of the TFA category (Typed First-order with Arithmetic)
at the CADE Automated Theorem Prover Competition 2013
with SPASS+T.
Winner of the TFA category (Typed First-order with Arithmetic)
at the CADE Automated Theorem Prover Competition 2011
with SPASS+T.