| Publication | Date of Publication | Type |
|---|
| A complete semantic back chaining proof system | 2023-04-28 | Paper |
| Conditional term rewriting and first-order theorem proving | 2023-03-09 | Paper |
| Polynomial time termination and constraint satisfaction tests | 2022-12-09 | Paper |
| The aspect calculus | 2020-03-10 | Paper |
| The search efficiency of theorem proving strategies | 2020-01-21 | Paper |
| Semantically guided first-order theorem proving using hyper-linking | 2020-01-21 | Paper |
| Semantically-guided goal-sensitive reasoning: inference system and completeness | 2018-04-03 | Paper |
| Semantically-guided goal-sensitive reasoning: model representation | 2016-05-26 | Paper |
| History and Prospects for First-Order Automated Deduction | 2015-12-02 | Paper |
| The Relative Power of Semantics and Unification | 2013-04-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3596461 | 2007-08-31 | Paper |
| Automated Reasoning with Analytic Tableaux and Related Methods | 2006-07-07 | Paper |
| A relevance restriction strategy for automated deduction | 2006-02-07 | Paper |
| A satisfiability procedure for quantified Boolean formulae | 2003-09-15 | Paper |
| Ordered semantic hyper tableaux | 2003-04-28 | Paper |
| Rewriting | 2002-08-27 | Paper |
| The complexity of some complementation problems | 2002-07-25 | Paper |
| General algorithms for permutations in equational inference | 2002-05-21 | Paper |
| Ordered semantic hyper-linking | 2001-02-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4503903 | 2000-09-14 | Paper |
| Theory of partial-order programming | 2000-06-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4314599 | 2000-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4949919 | 2000-05-07 | Paper |
| Special cases and substitutes for rigid \(E\)-unification | 2000-03-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4375764 | 1998-07-13 | Paper |
| Automated deduction techniques for classification in description logic systems | 1998-04-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4345253 | 1997-07-22 | Paper |
| Proof lengths for equational completion | 1996-12-12 | Paper |
| Problem solving by searching for models with a theorem prover | 1996-02-26 | Paper |
| On the mechanical derivation of loop invariants | 1995-01-12 | Paper |
| Correctness of unification without occur check in prolog | 1994-04-17 | Paper |
| Eliminating dublication with the hyper-linking strategy | 1994-01-02 | Paper |
| An algorithm for finding canonical sets of ground rewrite rules in polynomial time | 1993-05-16 | Paper |
| A semantic backward chaining proof system | 1992-09-27 | Paper |
| Rewrite, rewrite, rewrite, rewrite, rewrite, \dots | 1992-06-25 | Paper |
| Term rewriting: Some experimental results | 1991-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3484382 | 1990-01-01 | Paper |
| Rigid E-unification: NP-completeness and applications to equational matings | 1990-01-01 | Paper |
| A sequent-style model elimination strategy and a positive refinement | 1990-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3491006 | 1990-01-01 | Paper |
| A Heuristic Algorithm for Small Separators in Arbitrary Graphs | 1990-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4205073 | 1989-01-01 | Paper |
| Refinements to depth-first iterative-deepening search in automatic theorem proving | 1989-01-01 | Paper |
| Non-Horn clause logic programming without contrapositives | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3210187 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3817651 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3811749 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3805956 | 1988-01-01 | Paper |
| A heuristic triangulation algorithm | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3028319 | 1987-01-01 | Paper |
| A structure-preserving clause form translation | 1986-01-01 | Paper |
| A decision procedure for combinations of propositional temporal logic and other specialized theories | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3783520 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3783620 | 1986-01-01 | Paper |
| Termination orderings for associative-commutative rewriting systems | 1985-01-01 | Paper |
| Semantic confluence tests and completion methods | 1985-01-01 | Paper |
| The undecidability of self-embedding for term rewriting systems | 1985-01-01 | Paper |
| Complete divisibility problems for slowly utilized oracles | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3696500 | 1985-01-01 | Paper |
| New NP-hard and NP-complete polynomial and integer divisibility problems | 1984-01-01 | Paper |
| Heuristic matching for graphs satisfying the triangle inequality | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3696491 | 1984-01-01 | Paper |
| The occur-check problem in Prolog | 1984-01-01 | Paper |
| Complete problems in the first-order predicate calculus | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3336731 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3678693 | 1984-01-01 | Paper |
| The Travelling Salesman Problem and Minimum Matching in the Unit Square | 1983-01-01 | Paper |
| A simplified problem reduction format | 1982-01-01 | Paper |
| Theorem proving with abstraction | 1981-01-01 | Paper |
| An NP-complete matching problem | 1980-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3885237 | 1980-01-01 | Paper |
| The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability | 1980-01-01 | Paper |
| Fast verification, testing, and generation of large primes | 1979-01-01 | Paper |
| Some Polynomial and Integer Divisibility Problems are $NP$-Hard | 1978-01-01 | Paper |
| Sparse complex polynomials and polynomial reducibility | 1977-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4130962 | 1972-01-01 | Paper |
