Uwe Waldmann - RankMe

59 papers A* 1A 14B 8Journal 25Unranked 10

Year	Rank	Type	Title / Venue / Authors
2025	A	`ed.`	Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings CADE Clark W. Barrett, Uwe Waldmann
2025	J	`jnl`	Optimistic Higher-Order Superposition. CoRR Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger, Uwe Waldmann
2024	B	`conf`	A Modular Formalization of Superposition in Isabelle/HOL. ITP Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret
2024	—	`conf`	On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus. IJCAR (1) Uwe Waldmann
2024	J	`jnl`	On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus. CoRR Uwe Waldmann
2023	J	`jnl`	Complete and Efficient Higher-Order Reasoning via Lambda-Superposition. ACM SIGLOG News Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann
2023	J	`jnl`	Mechanical Mathematicians. Commun. ACM Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2022	J	`jnl`	A Comprehensive Framework for Saturation Theorem Proving. J. Autom. Reason. Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
2021	J	`jnl`	Superposition for Lambda-Free Higher-Order Logic. Log. Methods Comput. Sci. Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
2021	J	`jnl`	Superposition with Lambdas. CoRR Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2021	J	`jnl`	Superposition with Lambdas. J. Autom. Reason. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2020	—	`conf`	A Comprehensive Framework for Saturation Theorem Proving. IJCAR (1) Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
2020	J	`jnl`	Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. J. Autom. Reason. Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann
2020	J	`jnl`	Superposition for Lambda-Free Higher-Order Logic. CoRR Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
2019	—	`conf`	Hierarchic Superposition Revisited. Description Logic, Theory Combination, and All That Peter Baumgartner, Uwe Waldmann
2019	J	`jnl`	Hierarchic Superposition Revisited. CoRR Peter Baumgartner, Uwe Waldmann
2019	A	`conf`	Superposition with Lambdas. CADE Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2018	J	`jnl`	Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
2018	A	`conf`	Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann
2018	A	`conf`	Superposition for Lambda-Free Higher-Order Logic. IJCAR Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann
2017	B	`conf`	A Lambda-Free Higher-Order Recursive Path Order. FoSSaCS Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
2017	A	`conf`	A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. CADE Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
2017	—	`conf`	Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann
2017	J	`jnl`	Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement. Sci. Comput. Program. Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2016	J	`jnl`	Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
2016	J	`jnl`	Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand
2015	A	`conf`	Beagle - A Hierarchic Superposition Theorem Prover. CADE Peter Baumgartner, Joshua Bax, Uwe Waldmann
2015	J	`jnl`	Foreword to the Special Focus on Constraints and Combinations. Math. Comput. Sci. Pascal Fontaine, Thomas Sturm, Uwe Waldmann
2015	B	`conf`	Modal Tableau Systems with Blocking and Congruence Closure. TABLEAUX Renate A. Schmidt, Uwe Waldmann
2014	A	`conf`	Finite Quantification in Hierarchic Theorem Proving. IJCAR Peter Baumgartner, Joshua Bax, Uwe Waldmann
2014	—	`conf`	Hierarchic Superposition Revisited. PAAR@IJCAR Uwe Waldmann
2013	—	`conf`	From Search to Computation: Redundancy Criteria and Simplification at Work. Programming Logics Thomas Hillenbrand, Ruzica Piskac, Uwe Waldmann, Christoph Weidenbach
2013	A	`conf`	Hierarchic Superposition with Weak Abstraction. CADE Peter Baumgartner, Uwe Waldmann
2012	J	`jnl`	Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Sci. Comput. Program. Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2011	J	`jnl`	A Combined Superposition and Model Evolution Calculus. J. Autom. Reason. Peter Baumgartner, Uwe Waldmann
2009	A	`conf`	Superposition and Model Evolution Combined. CADE Peter Baumgartner, Uwe Waldmann
2007	B	`conf`	An Extension of the Knuth-Bendix Ordering with LPO-Like Properties. LPAR Michel Ludwig, Uwe Waldmann
2007	J	`jnl`	Comparing Instance Generation Methods for Automated Reasoning. J. Autom. Reason. Swen Jacobs, Uwe Waldmann
2007	B	`conf`	Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space. ATVA Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2006	B	`conf`	Automatic Verification of Hybrid Systems with Large Discrete State Space. ATVA Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
2006	J	`jnl`	Modular proof systems for partial functions with Evans equality. Inf. Comput. Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann
2005	B	`conf`	Comparing Instance Generation Methods for Automated Reasoning. TABLEAUX Swen Jacobs, Uwe Waldmann
2004	A	`conf`	Modular Proof Systems for Partial Functions with Weak Equality. IJCAR Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann
2003	A	`conf`	Superposition Modulo a Shostak Theory. CADE Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann
2002	J	`jnl`	Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I). J. Symb. Comput. Uwe Waldmann
2002	J	`jnl`	Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II). J. Symb. Comput. Uwe Waldmann
2001	A	`conf`	Superposition and Chaining for Totally Ordered Divisible Abelian Groups. IJCAR Uwe Waldmann
1999	B	`conf`	Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups. LPAR Uwe Waldmann
1998	J	`jnl`	Extending Reduction Orderings to ACU-Compatible Reduction Orderings. Inf. Process. Lett. Uwe Waldmann
1998	A	`conf`	Superposition for Divisible Torsion-Free Abelian Groups. CADE Uwe Waldmann
1997	—	`—`	Cancellative Abelian monoids in refutational theorem proving. Uwe Waldmann
1996	A	`conf`	Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). CADE Harald Ganzinger, Uwe Waldmann
1994	J	`jnl`	Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1993	A*	`conf`	Set Constraints are the Monadic Class LICS Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1993	—	`conf`	Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. Kurt Gödel Colloquium Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1992	J	`jnl`	Semantics of Order-Sorted Specifications. Theor. Comput. Sci. Uwe Waldmann
1992	—	`conf`	Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems. CTRS Harald Ganzinger, Uwe Waldmann
1992	—	`conf`	Theorem Proving for Hierarchic First-Order Theories. ALP Leo Bachmair, Harald Ganzinger, Uwe Waldmann
1990	—	`conf`	Compatibility of Order-Sorted Rewrite Rules. CTRS Uwe Waldmann