| SPASS Version 3.5 C Weidenbach, D Dimova, A Fietzke, R Kumar, M Suda, P Wischnewski Automated Deduction–CADE-22: 22nd International Conference on Automated …, 2009 | 427 | 2009 |
| Computing small clause normal forms A Nonnengart, C Weidenbach Handbook of automated reasoning, 335-367, 2001 | 313 | 2001 |
| SPASS: Combining superposition, sorts and splitting C Weidenbach Handbook of automated reasoning 2, 1965-2013, 1999 | 295 | 1999 |
| Towards an automatic analysis of security protocols in first-order logic H Ganzinger, C Weidenbach Automated Deduction—CADE-16: 16th International Conference on Automated …, 1999 | 254 | 1999 |
| Spass Version 2.0 C Weidenbach, U Brahm, T Hillenbrand, E Keen, C Theobald, D Topić Automated Deduction—CADE-18: 18th International Conference on Automated …, 2002 | 213 | 2002 |
| System description: SPASS version 1.0. 0 C Weidenbach, B Afshordel, U Brahm, C Cohrs, T Engel, E Keen, ... CADE, 378-382, 1999 | 209* | 1999 |
| Spass & flotter version 0.42 C Weidenbach, B Gaede, G Rock Automated Deduction—Cade-13: 13th International Conference on Automated …, 1996 | 174 | 1996 |
| On generating small clause normal forms A Nonnengart, G Rock, C Weidenbach Automated Deduction—CADE-15: 15th International Conference on Automated …, 1998 | 93 | 1998 |
| A verified SAT solver framework with learn, forget, restart, and incrementality JC Blanchette, M Fleury, P Lammich, C Weidenbach Journal of automated reasoning 61, 333-365, 2018 | 86 | 2018 |
| SPASS-Version 0.49 C Weidenbach Journal of Automated Reasoning 18, 247-252, 1997 | 79 | 1997 |
| Superposition modulo linear arithmetic SUP (LA) E Althaus, E Kruglov, C Weidenbach Frontiers of Combining Systems: 7th International Symposium, FroCoS 2009 …, 2009 | 75 | 2009 |
| Saturation-based decision procedures for extensions of the guarded fragment Y Kazakov Universität des Saarlandes Saarbrücken, 2006 | 66 | 2006 |
| Towards Verification of the Pastry Protocol Using TLA + T Lu, S Merz, C Weidenbach International Conference on Formal Methods for Open Object-Based Distributed …, 2011 | 57 | 2011 |
| Soft typing for ordered resolution H Ganzinger, C Meyer, C Weidenbach Automated Deduction—CADE-14: 14th International Conference on Automated …, 1997 | 52 | 1997 |
| More SPASS with Isabelle: Superposition with hard sorts and configurable simplification JC Blanchette, A Popescu, D Wand, C Weidenbach Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 50 | 2012 |
| Unification in extensions of shallow equational theories F Jacquemard, C Meyer, C Weidenbach Rewriting Techniques and Applications: 9th International Conference, RTA-98 …, 1998 | 45 | 1998 |
| First-order tableaux with sorts C Weidenbach Logic Journal of the IGPL 3 (6), 887-906, 1995 | 43 | 1995 |
| A PLTL-prover based on labelled superposition with partial model guidance M Suda, C Weidenbach Automated Reasoning: 6th International Joint Conference, IJCAR 2012 …, 2012 | 40 | 2012 |
| MSPASS: Subsumption Testing with SPASS. U Hustadt, RA Schmidt, C Weidenbach Description Logics, 1999 | 39 | 1999 |
| Unification in sort theories and its applications C Weidenbach Annals of Mathematics and Artificial Intelligence 18, 261-293, 1996 | 37 | 1996 |
