# Publications

## Papers

*On the generation of quantified lemmas*

(with S. Hetzl, A. Leitsch, G. Reis, and D. Weller)

Journal of Automated Reasoning (2018)

pdf,
Springer

*Algorithmic compression of finite tree languages by rigid acyclic grammars*

(with S. Eberhard and S. Hetzl)

ACM Transactions on Computational Logic 18(4) (2017)

pdf,
ACM

*A metaprogramming framework for formal verification*

(with S. Ullrich, J. Roesch, J. Avigad, and L. de Moura)

Proceedings of the ACM on Programming Languages 1(ICFP) (2017)

pdf,
ACM

*System description: GAPT 2.0*

(with S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner, and S. Zivota)

IJCAR 2016, N. Olivetti and A. Tiwari (eds.), Springer LNCS 9706

pdf,
slides,
Springer

## Talks

*Extracting expansion trees from
resolution proofs with splitting and definitions*

Theory & Logic seminar at TU Wien,
January 17, 2018,
slides.

*The Lean Theorem Prover*

Alpine Verification Meeting 2017,
September 18, 2017,
slides,
materials.

*Complexity of decision problems on TRATGs*

Herbrandâ€™s Theorem Revisited (workshop),
May 5, 2017,
slides.

*The Lean Theorem Prover*

(with L. de Moura, J. Roesch, and S. Ullrich)

POPL 2017, January 16, 2017,
slides,
materials.

*Minimal grammars via MaxSAT*

Theory & Logic seminar at TU Wien,
April 13, 2016,
slides.

*Finding loop invariants using tree grammars*

Theory & Logic seminar at TU Wien,
January 28, 2015,
slides.

## Preprints

*Complexity of decision problems on totally rigid
acyclic tree grammars* (2018)

(with S. Eberhard and S. Hetzl)

pdf

*Efficient translation of sequent calculus proofs
into natural deduction proofs* (2018)

(with M. Schlaipfer)

pdf

*Fast cut-elimination using proof terms:
an empirical study* (2018)

pdf

*Extracting expansion trees from resolution
proofs with splitting and definitions* (2018)

pdf

*Tree grammars for induction on inductive data
types modulo equational theories* (2018)

(with S. Hetzl)

pdf