Leitsch, Alexander; Lolic, Anela Extraction of expansion trees. (English) Zbl 07038742 J. Autom. Reasoning 62, No. 3, 393-430 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{A. Leitsch} and \textit{A. Lolic}, J. Autom. Reasoning 62, No. 3, 393--430 (2019; Zbl 07038742) Full Text: DOI
Nipkow, Tobias; Brinkop, Hauke Amortized complexity verified. (English) Zbl 07038741 J. Autom. Reasoning 62, No. 3, 367-391 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{T. Nipkow} and \textit{H. Brinkop}, J. Autom. Reasoning 62, No. 3, 367--391 (2019; Zbl 07038741) Full Text: DOI
Charguéraud, Arthur; Pottier, François Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. (English) Zbl 07038740 J. Autom. Reasoning 62, No. 3, 331-365 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{A. Charguéraud} and \textit{F. Pottier}, J. Autom. Reasoning 62, No. 3, 331--365 (2019; Zbl 07038740) Full Text: DOI
Marić, Filip Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. (English) Zbl 07038739 J. Autom. Reasoning 62, No. 3, 301-329 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{F. Marić}, J. Autom. Reasoning 62, No. 3, 301--329 (2019; Zbl 07038739) Full Text: DOI