Larchey-Wendling, Dominique Constructive decision via redundancy-free proof-search. (English) Zbl 1468.03015 J. Autom. Reasoning 64, No. 7, 1197-1219 (2020). MSC: 03B35 03B25 03B47 03F03 68V20 PDFBibTeX XMLCite \textit{D. Larchey-Wendling}, J. Autom. Reasoning 64, No. 7, 1197--1219 (2020; Zbl 1468.03015) Full Text: DOI HAL
Miller, Dale Mechanized metatheory revisited. (English) Zbl 1468.68303 J. Autom. Reasoning 63, No. 3, 625-665 (2019). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{D. Miller}, J. Autom. Reasoning 63, No. 3, 625--665 (2019; Zbl 1468.68303) Full Text: DOI HAL
Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert Semi-intelligible Isar proofs from machine-generated proofs. (English) Zbl 1356.68178 J. Autom. Reasoning 56, No. 2, 155-200 (2016). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., J. Autom. Reasoning 56, No. 2, 155--200 (2016; Zbl 1356.68178) Full Text: DOI HAL
Zankl, Harald; Felgenhauer, Bertram; Middeldorp, Aart Labelings for decreasing diagrams. (English) Zbl 1315.68226 J. Autom. Reasoning 54, No. 2, 101-133 (2015). MSC: 68T15 68Q42 PDFBibTeX XMLCite \textit{H. Zankl} et al., J. Autom. Reasoning 54, No. 2, 101--133 (2015; Zbl 1315.68226) Full Text: DOI
Kaliszyk, Cezary; Urban, Josef Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). (English) Zbl 1314.68283 J. Autom. Reasoning 53, No. 2, 173-213 (2014); erratum ibid. 54, No. 1, 99 (2015). MSC: 68T15 68T05 PDFBibTeX XMLCite \textit{C. Kaliszyk} and \textit{J. Urban}, J. Autom. Reasoning 53, No. 2, 173--213 (2014; Zbl 1314.68283) Full Text: DOI arXiv
Hirokawa, Nao; Middeldorp, Aart Decreasing diagrams and relative termination. (English) Zbl 1243.68199 J. Autom. Reasoning 47, No. 4, 481-501 (2011). MSC: 68Q42 68T15 PDFBibTeX XMLCite \textit{N. Hirokawa} and \textit{A. Middeldorp}, J. Autom. Reasoning 47, No. 4, 481--501 (2011; Zbl 1243.68199) Full Text: DOI
Bezem, Marc; Hendriks, Dimitri On the mechanization of the proof of Hessenberg’s theorem in coherent logic. (English) Zbl 1140.03004 J. Autom. Reasoning 40, No. 1, 61-85 (2008). Reviewer: Nail Zamov (Kazan) MSC: 03B35 03B10 68T15 PDFBibTeX XMLCite \textit{M. Bezem} and \textit{D. Hendriks}, J. Autom. Reasoning 40, No. 1, 61--85 (2008; Zbl 1140.03004) Full Text: DOI Link
Bella, Giampaolo; Massacci, Fabio; Paulson, Lawrence C. Verifying the SET purchase protocols. (English) Zbl 1104.68465 J. Autom. Reasoning 36, No. 1-2, 5-37 (2006). MSC: 68P25 68T15 94A62 PDFBibTeX XMLCite \textit{G. Bella} et al., J. Autom. Reasoning 36, No. 1--2, 5--37 (2006; Zbl 1104.68465) Full Text: DOI