default search action
Uwe Waldmann
Person information
- affiliation: Max Planck Institute for Informatics, Saarbrücken, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c32]Uwe Waldmann
:
On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus. IJCAR (1) 2024: 244-261 - [c31]Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret:
A Modular Formalization of Superposition in Isabelle/HOL. ITP 2024: 12:1-12:20 - [i4]Uwe Waldmann:
On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus. CoRR abs/2405.03367 (2024) - 2023
- [j20]Alexander Bentkamp, Jasmin Blanchette
Mechanical Mathematicians. Commun. ACM 66(4): 80-90 (2023) - [j19]Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann:
Complete and Efficient Higher-Order Reasoning via Lambda-Superposition. ACM SIGLOG News 10(4): 25-40 (2023) - 2022
- [j18]Uwe Waldmann
A Comprehensive Framework for Saturation Theorem Proving. J. Autom. Reason. 66(4): 499-539 (2022) - 2021
- [j17]Alexander Bentkamp
Superposition with Lambdas. J. Autom. Reason. 65(7): 893-940 (2021) - [j16]Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. Log. Methods Comput. Sci. 17(2) (2021) - [i3]Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Superposition with Lambdas. CoRR abs/2102.00453 (2021) - 2020
- [j15]Anders Schlichtkrull
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. J. Autom. Reason. 64(7): 1169-1195 (2020) - [c30]Uwe Waldmann
A Comprehensive Framework for Saturation Theorem Proving. IJCAR (1) 2020: 316-334 - [i2]Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. CoRR abs/2005.02094 (2020)
2010 – 2019
- 2019
- [c29]Peter Baumgartner, Uwe Waldmann:
Hierarchic Superposition Revisited. Description Logic, Theory Combination, and All That 2019: 15-56 - [c28]Alexander Bentkamp
Superposition with Lambdas. CADE 2019: 55-73 - [i1]Peter Baumgartner, Uwe Waldmann:
Hierarchic Superposition Revisited. CoRR abs/1904.03776 (2019) - 2018
- [j14]Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018) - [c27]Alexander Bentkamp
Superposition for Lambda-Free Higher-Order Logic. IJCAR 2018: 28-46 - [c26]Anders Schlichtkrull, Jasmin Christian Blanchette
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR 2018: 89-107 - 2017
- [j13]Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz:
Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement. Sci. Comput. Program. 148: 123-160 (2017) - [c25]Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann:
Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE 2017: 16-23 - [c24]Heiko Becker, Jasmin Christian Blanchette
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. CADE 2017: 432-453 - [c23]Jasmin Christian Blanchette
A Lambda-Free Higher-Order Recursive Path Order. FoSSaCS 2017: 461-479 - 2016
- [j12]Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016) - [j11]Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016) - 2015
- [j10]Pascal Fontaine, Thomas Sturm
Foreword to the Special Focus on Constraints and Combinations. Math. Comput. Sci. 9(3): 265 (2015) - [c22]Peter Baumgartner, Joshua Bax, Uwe Waldmann:
Beagle - A Hierarchic Superposition Theorem Prover. CADE 2015: 367-377 - [c21]Renate A. Schmidt
Modal Tableau Systems with Blocking and Congruence Closure. TABLEAUX 2015: 38-53 - 2014
- [c20]Uwe Waldmann:
Hierarchic Superposition Revisited. PAAR@IJCAR 2014: 1 - [c19]Peter Baumgartner, Joshua Bax, Uwe Waldmann:
Finite Quantification in Hierarchic Theorem Proving. IJCAR 2014: 152-167 - 2013
- [c18]Thomas Hillenbrand, Ruzica Piskac
From Search to Computation: Redundancy Criteria and Simplification at Work. Programming Logics 2013: 169-193 - [c17]Peter Baumgartner, Uwe Waldmann:
Hierarchic Superposition with Weak Abstraction. CADE 2013: 39-57 - 2012
- [j9]Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz:
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Sci. Comput. Program. 77(10-11): 1122-1150 (2012) - 2011
- [j8]Peter Baumgartner, Uwe Waldmann:
A Combined Superposition and Model Evolution Calculus. J. Autom. Reason. 47(2): 191-227 (2011)
2000 – 2009
- 2009
- [c16]Peter Baumgartner, Uwe Waldmann:
Superposition and Model Evolution Combined. CADE 2009: 17-34 - 2007
- [j7]Swen Jacobs
Comparing Instance Generation Methods for Automated Reasoning. J. Autom. Reason. 38(1-3): 57-78 (2007) - [c15]Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs
Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space. ATVA 2007: 425-440 - [c14]Michel Ludwig, Uwe Waldmann:
An Extension of the Knuth-Bendix Ordering with LPO-Like Properties. LPAR 2007: 348-362 - 2006
- [j6]Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann:
Modular proof systems for partial functions with Evans equality. Inf. Comput. 204(10): 1453-1492 (2006) - [c13]Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz:
Automatic Verification of Hybrid Systems with Large Discrete State Space. ATVA 2006: 276-291 - 2005
- [c12]Swen Jacobs
Comparing Instance Generation Methods for Automated Reasoning. TABLEAUX 2005: 153-168 - 2004
- [c11]Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann:
Modular Proof Systems for Partial Functions with Weak Equality. IJCAR 2004: 168-182 - 2003
- [c10]Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann:
Superposition Modulo a Shostak Theory. CADE 2003: 182-196 - 2002
- [j5]Uwe Waldmann:
Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I). J. Symb. Comput. 33(6): 777-829 (2002) - [j4]Uwe Waldmann:
Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II). J. Symb. Comput. 33(6): 831-861 (2002) - 2001
- [c9]Uwe Waldmann:
Superposition and Chaining for Totally Ordered Divisible Abelian Groups. IJCAR 2001: 226-241
1990 – 1999
- 1999
- [c8]Uwe Waldmann:
Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups. LPAR 1999: 131-147 - 1998
- [j3]Uwe Waldmann:
Extending Reduction Orderings to ACU-Compatible Reduction Orderings. Inf. Process. Lett. 67(1): 43-49 (1998) - [c7]Uwe Waldmann:
Superposition for Divisible Torsion-Free Abelian Groups. CADE 1998: 144-159 - 1997
- [b1]Uwe Waldmann:
Cancellative Abelian monoids in refutational theorem proving. Saarland University, 1997, pp. 1-218 - 1996
- [c6]Harald Ganzinger, Uwe Waldmann:
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). CADE 1996: 388-402 - 1994
- [j2]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5: 193-212 (1994) - 1993
- [c5]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. Kurt Gödel Colloquium 1993: 83-96 - [c4]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Set Constraints are the Monadic Class. LICS 1993: 75-83 - 1992
- [j1]Uwe Waldmann:
Semantics of Order-Sorted Specifications. Theor. Comput. Sci. 94(1): 1-35 (1992) - [c3]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Theorem Proving for Hierarchic First-Order Theories. ALP 1992: 420-434 - [c2]Harald Ganzinger, Uwe Waldmann:
Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems. CTRS 1992: 430-437 - 1990
- [c1]Uwe Waldmann:
Compatibility of Order-Sorted Rewrite Rules. CTRS 1990: 407-416
Coauthor Index
aka: Jasmin Christian Blanchette
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-09-04 01:20 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: