Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal Scalable fine-grained proofs for formula processing. (English) Zbl 1468.68278 J. Autom. Reasoning 64, No. 3, 485-510 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{H. Barbosa} et al., J. Autom. Reasoning 64, No. 3, 485--510 (2020; Zbl 1468.68278) Full Text: DOI HAL
Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei Resolution proof transformation for compression and interpolation. (English) Zbl 1317.68123 Form. Methods Syst. Des. 45, No. 1, 1-41 (2014). MSC: 68Q60 03C40 03F20 68T15 PDFBibTeX XMLCite \textit{S. F. Rollini} et al., Form. Methods Syst. Des. 45, No. 1, 1--41 (2014; Zbl 1317.68123) Full Text: DOI arXiv
Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare SMT proof checking using a logical framework. (English) Zbl 1284.68521 Form. Methods Syst. Des. 42, No. 1, 91-118 (2013). MSC: 68T15 68T20 03B35 68Q55 PDFBibTeX XMLCite \textit{A. Stump} et al., Form. Methods Syst. Des. 42, No. 1, 91--118 (2013; Zbl 1284.68521) Full Text: DOI