| Modular proof systems for partial functions with Evans equality | 23 | 1.07 | 2006 |
| Superposition with equivalence reasoning and delayed clause normal form transformation | 12 | 0.92 | 2005 |
| Modular Proof Systems for Partial Functions with Weak Equality | 11 | 0.90 | 2004 |
| Fast Term Indexing with Coded Context Trees | 6 | 0.62 | 2004 |
| Superposition Modulo a Shostak Theory | 3 | 0.44 | 2003 |
| New directions in instantiation-based theorem proving | 50 | 1.81 | 2003 |
| Shostak Light | 22 | 2.12 | 2002 |
| Bottom-Up Deduction with Deletion and Priorities | 0 | 0.34 | 2001 |
| Efficient deductive methods for program analysis | 0 | 0.34 | 2001 |
| Automated complexity analysis based on ordered resolution | 36 | 1.53 | 2001 |
| A New Meta-complexity Theorem for Bottom-Up Logic Programs | 21 | 1.55 | 2001 |
| Chaining Techniques for Automated Theorem Proving in Many-Valued Logics | 10 | 0.57 | 2000 |
| Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification | 5 | 0.50 | 2000 |
| Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings | 36 | 5.80 | 1999 |
| Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings | 20 | 3.59 | 1999 |
| Decidable Fragments of Simultaneous Rigid Reachability | 2 | 0.39 | 1999 |
| Strict Basic Superposition | 4 | 0.48 | 1998 |
| A Resolution-Based Decision Procedure for Extensions of K4 | 15 | 0.95 | 1998 |
| Wohin geht die automatische Deduktion? | 0 | 0.34 | 1998 |
| Elimination of Equality via Transformation with Ordering Constraints | 12 | 0.66 | 1998 |
| Ordered chaining calculi for first-order theories of transitive relations | 32 | 1.70 | 1998 |
| Soft Typing for Ordered Resolution | 19 | 1.64 | 1997 |
| Theorem Proving in Cancellative Abelian Monoids (Extended Abstract) | 12 | 0.68 | 1996 |
| Saturation-Based Theorem Proving (Abstract) | 3 | 0.41 | 1996 |
| Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract) | 0 | 0.34 | 1996 |
| Complexity Analysis Based on Ordered Resolution | 14 | 1.06 | 1996 |
| Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings | 37 | 4.09 | 1996 |
| Basic paramodulation | 58 | 7.44 | 1995 |
| Buchberger's Algorithm: A Constraint-Based Completion Procedure | 15 | 1.12 | 1994 |
| Rewrite techniques for transitive relations | 25 | 1.24 | 1994 |
| Associative-Commutative Superposition | 16 | 1.04 | 1994 |
| Refutational Theorem Proving for Hierachic First-Order Theories | 29 | 1.20 | 1994 |
| Ordered Chaining for Total Orderings | 13 | 0.73 | 1994 |
| Rewrite-Based Equational Theorem Proving with Selection and Simplification | 203 | 14.06 | 1994 |
| Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings | 7 | 0.56 | 1994 |
| Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality | 37 | 1.95 | 1993 |
| Set constraints are the monadic class | 63 | 5.25 | 1993 |
| Program Development: Completion Subsystem | 0 | 0.34 | 1993 |
| Basic Paramodulation and Superposition | 59 | 7.59 | 1992 |
| Konferenzbericht LICS '92 | 0 | 0.34 | 1992 |
| Inductive Theorem Proving by Consistency for First-Order Clauses | 15 | 0.90 | 1992 |
| Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems | 27 | 1.47 | 1992 |
| Theorem Proving for Hierarchic First-Order Theories | 8 | 2.23 | 1992 |
| Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria | 13 | 0.84 | 1992 |
| Order-sorted completion: the many-sorted way | 25 | 1.67 | 1991 |
| Perfect Model Semantics For Logic Programs With Equality | 20 | 2.82 | 1991 |
| Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract) | 11 | 0.75 | 1990 |
| On Restrictions of Ordered Paramodulation with Simplification | 63 | 6.73 | 1990 |
| Order-Sorted Completion: The Many-Sorted Way (Extended Abstract) | 4 | 0.46 | 1989 |
| ESOP '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings | 27 | 8.52 | 1988 |
