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 | 112 | 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 | 68 | 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 |
An extensible user interface for Lean 4 W Nawrocki, EW Ayers, G Ebner 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 | 6 | 2023 |
A Unifying Splitting Framework. G Ebner, J Blanchette, S Tourret CADE, 344-360, 2021 | 6 | 2021 |
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 |