Follow
Gabriel Ebner
Gabriel Ebner
Carnegie Mellon University
Verified email at gebner.org - Homepage
Title
Cited by
Cited by
Year
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
852017
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
422016
Maintaining a library of formal mathematics
F Doorn, G Ebner, RY Lewis
International Conference on Intelligent Computer Mathematics, 251-267, 2020
172020
On the generation of quantified lemmas
G Ebner, S Hetzl, A Leitsch, G Reis, D Weller
Journal of Automated Reasoning 63 (1), 95-126, 2019
142019
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
142017
Complexity of decision problems on totally rigid acyclic tree grammars
S Eberhard, G Ebner, S Hetzl
42018
A Unifying Splitting Framework.
G Ebner, J Blanchette, S Tourret
CADE, 344-360, 2021
32021
Herbrand constructivization for automated intuitionistic theorem proving
G Ebner
International Conference on Automated Reasoning with Analytic Tableaux and …, 2019
32019
The Lean reference manual
J Avigad, G Ebner, S Ullrich
URL https://leanprover. github. io/reference/lean_reference. pdf, 2018
22018
Fast cut-elimination using proof terms: an empirical study
G Ebner
22018
Tree grammars for induction on inductive data types modulo equational theories
G Ebner, S Hetzl
22018
HyperTree Proof Search for Neural Theorem Proving
G Lample, MA Lachaux, T Lavril, X Martinet, A Hayat, G Ebner, ...
arXiv preprint arXiv:2205.11491, 2022
12022
A unifying splitting framework (technical report)
G Ebner, J Blanchette, S Tourret
Technical report, 2021
12021
Efficient translation of sequent calculus proofs into natural deduction proofs
G Ebner, M Schlaipfer
12018
Inductive theorem proving based on tree grammars
G Ebner
Wien, 2021
2021
Extracting expansion trees from resolution proofs with splitting and definitions
G Ebner
2018
The Lean Theorem Prover
G Ebner
2017
Finding loop invariants using tree grammars
G Ebner
2015
Inductive theorem proving using tree grammars
G Ebner
Induction formulas and term structure
G Ebner, S Hetzl
The system can't perform the operation now. Try again later.
Articles 1–20