| Proof Development with Ωmega J Siekmann, C Benzmüller, V Brezhnev, L Cheikhrouhou, A Fiedler, ... International Conference on Automated Deduction, 144-149, 2002 | 117 | 2002 |
| Descente infinie+ deduction CP Wirth Logic Journal of IGPL 12 (1), 1-96, 2004 | 88 | 2004 |
| How to Prove Inductive Theorems? QuodLibet! J Avenhaus, U Kühler, T Schmidt-Samoa, CP Wirth International Conference on Automated Deduction, 328-333, 2003 | 41 | 2003 |
| A constructor-based approach to positive/negative-conditional equational specifications CP Wirth, B Gramlich Journal of Symbolic Computation 17 (1), 51-90, 1994 | 40 | 1994 |
| A generic modular data structure for proof attempts alternating on ideas and granularity S Autexier, C Benzmüller, D Dietrich, A Meier, CP Wirth International Conference on Mathematical Knowledge Management, 126-142, 2005 | 35 | 2005 |
| Positive/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving. Schriftenreihe Forschungsergebnisse zur Informatik, ISBN … CP Wirth Verlag Dr. Kovac, Hamburg 31, 250, 1997 | 32* | 1997 |
| Conditional equational specifications of data types with partial operations for inductive theorem proving U Kühler, CP Wirth International Conference on Rewriting Techniques and Applications, 38-52, 1997 | 29 | 1997 |
| Hilbert's epsilon as an operator of indefinite committed choice CP Wirth Journal of Applied Logic 6 (3), 287-317, 2008 | 27* | 2008 |
| On notions of inductive validity for first-order equational clauses CP Wirth, B Gramlich International Conference on Automated Deduction, 162-176, 1994 | 27 | 1994 |
| History and future of implicit and inductionless induction: beware the old jade and the zombie! CP Wirth Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on …, 2005 | 23 | 2005 |
| Grundlagen der Mathematik= Foundations of mathematics D Hilbert, P Bernays, CP Wirth, J Siekmann, M Gabbay, D Gabbay (No Title), 1934 | 23 | 1934 |
| On Notions of Inductive Validity for First-Order Equational Clauses. 12th CADE 1994, LNAI 814 CP Wirth, B Gramlich Springer, 1994 | 21 | 1994 |
| Abstract notions and inference systems for proofs by mathematical induction CP Wirth, K Becker International Workshop on Conditional Term Rewriting Systems, 353-373, 1994 | 19 | 1994 |
| Assuring automotive data and software integrity employing distributed hash tables and blockchain G Falco, JE Siegel arXiv preprint arXiv:2002.02780, 2020 | 18* | 2020 |
| Syntactic confluence criteria for positive/negative-conditional term rewriting systems CP Wirth arXiv preprint arXiv:0902.3614, 2009 | 16 | 2009 |
| Jacques Herbrand: Life, Logic, and Automated Deduction. CP Wirth, JH Siekmann, C Benzmüller, S Autexier Logic from Russell to Church 5, 195-254, 2009 | 16 | 2009 |
| Shallow confluence of conditional term rewriting systems CP Wirth Journal of Symbolic Computation 44 (1), 60-98, 2009 | 16 | 2009 |
| Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization CP Wirth International Workshop on First-Order Theorem Proving, 282-297, 1998 | 15 | 1998 |
| Grundlagen der Mathematik I: Prefaces and [par][par] 1-2 D Hilbert, P Bernays, CP Wirth College, 2011 | 11 | 2011 |
| A new indefinite semantics for Hilbert’s epsilon CP Wirth International Conference on Automated Reasoning with Analytic Tableaux and …, 2002 | 11 | 2002 |
Christoph BenzmüllerProfessor for AI Systems Engineering, University of BambergVerified email at fu-berlin.de
