Uwe Waldmann

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

2023

Complete and Efficient Higher-Order Reasoning via Lambda-Superposition.

[BibT_eX]

[DOI]

ACM SIGLOG News, October, 2023

Mechanical Mathematicians.

[BibT_eX]

[DOI]

Commun. ACM, 2023

2022

A Comprehensive Framework for Saturation Theorem Proving.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

2021

Superposition for Lambda-Free Higher-Order Logic.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2021

Superposition with Lambdas.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

2020

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

2019

Hierarchic Superposition Revisited.

[BibT_eX]

[DOI]

Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover.

[BibT_eX]

[DOI]

Anders Schlichtkrull

Dmitriy Traytel

Arch. Formal Proofs, 2018

2017

Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2017

A Lambda-Free Higher-Order Recursive Path Order.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2017

Towards Strong Higher-Order Automation for Fast Interactive Verification.

[BibT_eX]

[DOI]

Pascal Fontaine

Stephan Schulz

Proceedings of the ARCADE 2017, 2017

A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms.

[BibT_eX]

[DOI]

Heiko Becker

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms.

[BibT_eX]

[DOI]

Heiko Becker

Arch. Formal Proofs, 2016

2015

Foreword to the Special Focus on Constraints and Combinations.

[BibT_eX]

[DOI]

Pascal Fontaine

Thomas Sturm

Math. Comput. Sci., 2015

Modal Tableau Systems with Blocking and Congruence Closure.

[BibT_eX]

[DOI]

Renate A. Schmidt

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Beagle - A Hierarchic Superposition Theorem Prover.

[BibT_eX]

[DOI]

Joshua Bax

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Hierarchic Superposition Revisited.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

Finite Quantification in Hierarchic Theorem Proving.

[BibT_eX]

[DOI]

Joshua Bax

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Hierarchic Superposition with Weak Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

From Search to Computation: Redundancy Criteria and Simplification at Work.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2012

2011

A Combined Superposition and Model Evolution Calculus.

[BibT_eX]

[DOI]

J. Autom. Reason., 2011

2009

Superposition and Model Evolution Combined.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2007

Comparing Instance Generation Methods for Automated Reasoning.

[BibT_eX]

[DOI]

Swen Jacobs

J. Autom. Reason., 2007

An Extension of the Knuth-Bendix Ordering with LPO-Like Properties.

[BibT_eX]

[DOI]

Michel Ludwig

Proceedings of the Logic for Programming, 2007

Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2007

2006

Modular proof systems for partial functions with Evans equality.

[BibT_eX]

[DOI]

Viorica Sofronie-Stokkermans

Inf. Comput., 2006

Automatic Verification of Hybrid Systems with Large Discrete State Space.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

2004

Modular Proof Systems for Partial Functions with Weak Equality.

[BibT_eX]

[DOI]

Viorica Sofronie-Stokkermans

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Superposition Modulo a Shostak Theory.

[BibT_eX]

[DOI]

Thomas Hillenbrand

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II).

[BibT_eX]

[DOI]

J. Symb. Comput., 2002

Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I).

[BibT_eX]

[DOI]

J. Symb. Comput., 2002

2001

Superposition and Chaining for Totally Ordered Divisible Abelian Groups.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

1999

Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Automated Reasoning, 6th International Conference, 1999

1998

Extending Reduction Orderings to ACU-Compatible Reduction Orderings.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1998

Superposition for Divisible Torsion-Free Abelian Groups.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

1997

Cancellative Abelian monoids in refutational theorem proving.

[BibT_eX]

[DOI]

PhD thesis, 1997

1996

Theorem Proving in Cancellative Abelian Monoids (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1994

Refutational Theorem Proving for Hierarchic First-Order Theories.

[BibT_eX]

[DOI]

Appl. Algebra Eng. Commun. Comput., 1994

1993

Set Constraints are the Monadic Class

[BibT_eX]

[DOI]

Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, 1993

1992

Semantics of Order-Sorted Specifications.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1992

Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Theorem Proving for Hierarchic First-Order Theories.

[BibT_eX]

[DOI]

Proceedings of the Algebraic and Logic Programming, 1992

1990

Compatibility of Order-Sorted Rewrite Rules.

[BibT_eX]

[DOI]