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 | 85 | 2017 |

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 | 42 | 2016 |

Maintaining a library of formal mathematics F Doorn, G Ebner, RY Lewis International Conference on Intelligent Computer Mathematics, 251-267, 2020 | 17 | 2020 |

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 | 14 | 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 |

Complexity of decision problems on totally rigid acyclic tree grammars S Eberhard, G Ebner, S Hetzl | 4 | 2018 |

A Unifying Splitting Framework. G Ebner, J Blanchette, S Tourret CADE, 344-360, 2021 | 3 | 2021 |

Herbrand constructivization for automated intuitionistic theorem proving G Ebner International Conference on Automated Reasoning with Analytic Tableaux and …, 2019 | 3 | 2019 |

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 |

Tree grammars for induction on inductive data types modulo equational theories G Ebner, S Hetzl | 2 | 2018 |

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 | 1 | 2022 |

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 |

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 | | |