| A metaprogramming framework for formal verification G Ebner, S Ullrich, J Roesch, J Avigad, L de Moura Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017 | 111 | 2017 |
| Hypertree proof search for neural theorem proving G Lample, T Lacroix, MA Lachaux, A Rodriguez, A Hayat, T Lavril, ... Advances in neural information processing systems 35, 26337-26349, 2022 | 66 | 2022 |
| System description: GAPT 2.0 G Ebner, S Hetzl, G Reis, M Riener, S Wolfsteiner, S Zivota International Joint Conference on Automated Reasoning, 293-301, 2016 | 43 | 2016 |
| Maintaining a library of formal mathematics F van Doorn, G Ebner, RY Lewis International Conference on Intelligent Computer Mathematics, 251-267, 2020 | 30 | 2020 |
| On the generation of quantified lemmas G Ebner, S Hetzl, A Leitsch, G Reis, D Weller Journal of Automated Reasoning 63, 95-126, 2019 | 15 | 2019 |
| Algorithmic compression of finite tree languages by rigid acyclic grammars S Eberhard, G Ebner, S Hetzl ACM Transactions on Computational Logic (TOCL) 18 (4), 1-20, 2017 | 14 | 2017 |
| A Unifying Splitting Framework. G Ebner, J Blanchette, S Tourret CADE, 344-360, 2021 | 6 | 2021 |
| An extensible user interface for Lean 4 W Nawrocki, EW Ayers, G Ebner 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 | 5 | 2023 |
| Herbrand constructivization for automated intuitionistic theorem proving G Ebner Automated Reasoning with Analytic Tableaux and Related Methods: 28th …, 2019 | 4 | 2019 |
| Complexity of decision problems on totally rigid acyclic tree grammars S Eberhard, G Ebner, S Hetzl | 4 | 2018 |
| The Lean reference manual J Avigad, G Ebner, S Ullrich URL https://leanprover. github. io/reference/lean_reference. pdf, 2018 | 2 | 2018 |
| Fast cut-elimination using proof terms: an empirical study G Ebner | 2 | 2018 |
| Lean Formalization of Extended Regular Expression Matching with Lookarounds E Zhuchko, M Veanes, G Ebner Proceedings of the 13th ACM SIGPLAN International Conference on Certified …, 2024 | 1 | 2024 |
| A unifying splitting framework (technical report) G Ebner, J Blanchette, S Tourret Technical report, 2021 | 1 | 2021 |
| Efficient translation of sequent calculus proofs into natural deduction proofs G Ebner, M Schlaipfer | 1 | 2018 |
| Tree grammars for induction on inductive data types modulo equational theories G Ebner, S Hetzl | 1 | 2018 |
| Symbolic Automata: -Regularity Modulo Theories M Veanes, T Ball, G Ebner, O Saarikivi arXiv preprint arXiv:2310.02393, 2023 | | 2023 |
| Unifying Splitting G Ebner, J Blanchette, S Tourret Journal of Automated Reasoning 67 (2), 16, 2023 | | 2023 |
| Inductive theorem proving based on tree grammars G Ebner Technische Universität Wien, 2021 | | 2021 |
| Extracting expansion trees from resolution proofs with splitting and definitions G Ebner | | 2018 |
