| Publication | Date of Publication | Type |
|---|
Termination proofs of well-moded logic programs via conditional rewrite systems
Conditional Term Rewriting Systems | 2023-03-09 | Paper |
Compatibility of order-sorted rewrite rules
Conditional and Typed Rewriting Systems | 2023-03-09 | Paper |
A comprehensive framework for saturation theorem proving
Journal of Automated Reasoning | 2022-12-12 | Paper |
A comprehensive framework for saturation theorem proving
Automated Reasoning | 2022-11-09 | Paper |
Superposition with lambdas
Journal of Automated Reasoning | 2021-11-24 | Paper |
scientific article; zbMATH DE number 7350767 (Why is no real title available?)
| 2021-05-25 | Paper |
Formalizing Bachmair and Ganzinger's ordered resolution prover
Journal of Automated Reasoning | 2020-11-02 | Paper |
Hierarchic superposition revisited
| 2020-06-04 | Paper |
Superposition with lambdas
Lecture Notes in Computer Science | 2020-03-10 | Paper |
Theorem proving in cancellative abelian monoids (extended abstract)
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
Formalizing Bachmair and Ganzinger's ordered resolution prover
Automated Reasoning | 2018-10-18 | Paper |
Superposition for \(\lambda\)-free higher-order logic
| 2018-10-18 | Paper |
A transfinite Knuth-Bendix order for lambda-free higher-order terms
| 2017-09-22 | Paper |
A Lambda-Free Higher-Order Recursive Path Order
Lecture Notes in Computer Science | 2017-05-19 | Paper |
Extending reduction orderings to ACU-compatible reduction orderings
Information Processing Letters | 2016-06-09 | Paper |
Modal tableau systems with blocking and congruence closure
Lecture Notes in Computer Science | 2015-12-11 | Paper |
Beagle -- a hierarchic superposition theorem prover
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Finite Quantification in Hierarchic Theorem Proving
Automated Reasoning | 2014-09-26 | Paper |
Hierarchic superposition with weak abstraction
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
From search to computation: redundancy criteria and simplification at work
Programming Logics | 2013-04-19 | Paper |
A combined superposition and model evolution calculus
Journal of Automated Reasoning | 2012-07-31 | Paper |
Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
Science of Computer Programming | 2012-07-20 | Paper |
Superposition modulo a Shostak theory.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Superposition and Model Evolution Combined
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Automatic Verification of Hybrid Systems with Large Discrete State Space
Automated Technology for Verification and Analysis | 2008-09-04 | Paper |
Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
Automated Technology for Verification and Analysis | 2008-07-03 | Paper |
An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Comparing instance generation methods for automated reasoning
Journal of Automated Reasoning | 2007-05-04 | Paper |
Modular proof systems for partial functions with Evans equality
Information and Computation | 2006-10-25 | Paper |
Automated Reasoning with Analytic Tableaux and Related Methods
Lecture Notes in Computer Science | 2006-07-07 | Paper |
Cancellative Abelian monoids and related structures in refutational theorem proving. II
Journal of Symbolic Computation | 2003-03-23 | Paper |
Cancellative Abelian monoids and related structures in refutational theorem proving. I
Journal of Symbolic Computation | 2003-03-23 | Paper |
scientific article; zbMATH DE number 1765672 (Why is no real title available?)
| 2002-07-10 | Paper |
scientific article; zbMATH DE number 1405448 (Why is no real title available?)
| 2000-07-13 | Paper |
scientific article; zbMATH DE number 1300967 (Why is no real title available?)
| 1999-07-29 | Paper |
scientific article; zbMATH DE number 1303342 (Why is no real title available?)
| 1999-06-17 | Paper |
Refutational theorem proving for hierarchic first-order theories
Applicable Algebra in Engineering, Communication and Computing | 1994-07-04 | Paper |
scientific article; zbMATH DE number 517065 (Why is no real title available?)
| 1994-04-17 | Paper |
Semantics of order-sorted specifications
Theoretical Computer Science | 1992-06-28 | Paper |
