| Superposition with lambdas A Bentkamp, J Blanchette, S Tourret, P Vukmirović, U Waldmann Journal of Automated Reasoning 65 (7), 893-940, 2021 | 56 | 2021 |
| Superposition for lambda-free higher-order logic A Bentkamp, J Blanchette, S Cruanes, U Waldmann Logical Methods in Computer Science 17, 2021 | 56 | 2021 |
| Making Higher-Order Superposition Work. P Vukmirovic, A Bentkamp, J Blanchette, S Cruanes, V Nummelin, ... CADE, 415-432, 2021 | 37 | 2021 |
| Efficient full higher-order unification P Vukmirović, A Bentkamp, V Nummelin Logical Methods in Computer Science 17, 2021 | 30 | 2021 |
| Superposition for Full Higher-order Logic. A Bentkamp, J Blanchette, S Tourret, P Vukmirovic CADE, 396-412, 2021 | 29 | 2021 |
| Superposition for higher-order logic A Bentkamp, J Blanchette, S Tourret, P Vukmirović Journal of Automated Reasoning 67 (1), 10, 2023 | 20 | 2023 |
| A formal proof of the expressiveness of deep learning A Bentkamp, JC Blanchette, D Klakow Journal of Automated Reasoning 63, 347-368, 2019 | 20 | 2019 |
| HHLPy: practical verification of hybrid systems using Hoare logic H Sheng, A Bentkamp, B Zhan International Symposium on Formal Methods, 160-178, 2023 | 15 | 2023 |
| Superposition with First-class Booleans and Inprocessing Clausification. V Nummelin, A Bentkamp, S Tourret, P Vukmirovic CADE, 378-395, 2021 | 15 | 2021 |
| Mechanical mathematicians A Bentkamp, J Blanchette, V Nummelin, S Tourret, P Vukmirović, ... Communications of the ACM 66 (4), 80-90, 2023 | 11 | 2023 |
| Verified reductions for optimization A Bentkamp, RF Mir, J Avigad International Conference on Tools and Algorithms for the Construction and …, 2023 | 8 | 2023 |
| Executable multivariate polynomials. Archive of Formal Proofs, August 2010 C Sternagel, R Thiemann, A Maletzky, F Immler, F Haftmann, A Lochbihler, ... | 7 | |
| The Hitchhiker’s guide to logical verification A Baanen, A Bentkamp, J Blanchette, J Hölzl, J Limperg Vrije Universiteit Amsterdam, 2021 | 6 | 2021 |
| Superposition with first-class Booleans and inprocessing clausification (technical report) V Nummelin, A Bentkamp, S Tourret, P Vukmirović Technical report, 2021. https://matryoshka-project. github. io/pubs …, 2021 | 5 | 2021 |
| Formalization of the embedding path order for lambda-free higher-order terms. Archive of Formal Proofs (2018) A Bentkamp | 5 | 2018 |
| ARCH-COMP22 category report: Hybrid systems theorem proving S Mitsch, B Zhan, H Sheng, A Bentkamp, X Jin, S Wang, S Foster, ... ARCH22 90, 185-203, 2022 | 4 | 2022 |
| Superposition with lambdas (technical report) A Bentkamp, J Blanchette, S Tourret, P Vukmirović, U Waldmann Technical report, 2019 | 4 | 2019 |
| Superposition for lambda-free higher-order logic (technical report) A Bentkamp, JC Blanchette, S Cruanes, U Waldmann Technical report, 2018 | 4 | 2018 |
| The Embedding Path Order for Lambda-Free Higher-Order Terms. A Bentkamp FLAP 8 (10), 2447-2470, 2021 | 3 | 2021 |
| Superposition for full higherorder logic (technical report) A Bentkamp, JC Blanchette, S Tourret, P Vukmirovic Technical report, 2021 | 3 | 2021 |
