Raggi, Daniel; Stockdill, Aaron; Jamnik, Mateja; Garcia Garcia, Grecia; Sutherland, Holly E. A.; Cheng, Peter C.-H. Inspection and selection of representations. (English) Zbl 1428.68293 Kaliszyk, Cezary (ed.) et al., Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11617, 227-242 (2019). MSC: 68T35 68T30 PDFBibTeX XMLCite \textit{D. Raggi} et al., Lect. Notes Comput. Sci. 11617, 227--242 (2019; Zbl 1428.68293) Full Text: DOI Link
Farmer, William M. Incorporating quotation and evaluation into Church’s type theory. (English) Zbl 1390.68168 Inf. Comput. 260, 9-50 (2018). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{W. M. Farmer}, Inf. Comput. 260, 9--50 (2018; Zbl 1390.68168) Full Text: DOI arXiv
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef Hammering towards QED. (English) Zbl 1451.68318 J. Formaliz. Reason. 9, No. 1, 101-148 (2016). MSC: 68V15 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., J. Formaliz. Reason. 9, No. 1, 101--148 (2016; Zbl 1451.68318) Full Text: DOI
Maletzky, Alexander Mathematical theory exploration in Theorema: reduction rings. (English) Zbl 1344.68210 Kohlhase, Michael (ed.) et al., Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-42546-7/pbk; 978-3-319-42547-4/ebook). Lecture Notes in Computer Science 9791. Lecture Notes in Artificial Intelligence, 3-17 (2016). MSC: 68T15 13P10 PDFBibTeX XMLCite \textit{A. Maletzky}, Lect. Notes Comput. Sci. 9791, 3--17 (2016; Zbl 1344.68210) Full Text: DOI arXiv
Omodeo, Eugenio G.; Tomescu, Alexandru I. Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets. (English) Zbl 1315.68223 J. Autom. Reasoning 52, No. 1, 1-29 (2014). MSC: 68T15 03B35 05C75 PDFBibTeX XMLCite \textit{E. G. Omodeo} and \textit{A. I. Tomescu}, J. Autom. Reasoning 52, No. 1, 1--29 (2014; Zbl 1315.68223) 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
Lambán, Laureano; Martín-Mateos, Francisco-Jesús; Rubio, Julio; Ruiz-Reina, José-Luis Formalization of a normalization theorem in simplicial topology. (English) Zbl 1280.68232 Ann. Math. Artif. Intell. 64, No. 1, 1-37 (2012). MSC: 68T15 68W30 55U10 PDFBibTeX XMLCite \textit{L. Lambán} et al., Ann. Math. Artif. Intell. 64, No. 1, 1--37 (2012; Zbl 1280.68232) Full Text: DOI Link
Gordon, Michael J. C.; Kaufmann, Matt; Ray, Sandip The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4. (English) Zbl 1216.68233 J. Autom. Reasoning 47, No. 1, 1-16 (2011). MSC: 68T15 03B44 68Q60 PDFBibTeX XMLCite \textit{M. J. C. Gordon} et al., J. Autom. Reasoning 47, No. 1, 1--16 (2011; Zbl 1216.68233) Full Text: DOI
Araújo, João; McCune, William Computer solutions of problems in inverse semigroups. (English) Zbl 1202.20065 Commun. Algebra 38, No. 3, 1104-1121 (2010). Reviewer: Jaak Henno (Tallinn) MSC: 20M18 20M07 20M05 20A05 68T15 03B35 PDFBibTeX XMLCite \textit{J. Araújo} and \textit{W. McCune}, Commun. Algebra 38, No. 3, 1104--1121 (2010; Zbl 1202.20065) Full Text: DOI
Ridge, Thomas Verifying distributed systems: the operational approach. (English) Zbl 1315.68105 Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 429-440 (2009). MSC: 68N30 68N19 68M14 68Q60 68T15 PDFBibTeX XMLCite \textit{T. Ridge}, in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '09, Savannah, GA, USA, January 18--24, 2009. New York, NY: Association for Computing Machinery (ACM). 429--440 (2009; Zbl 1315.68105) Full Text: DOI
Kaufmann, Matt; Moore, J Strother; Ray, Sandip; Reeber, Erik Integrating external deduction tools with ACL2. (English) Zbl 1183.68558 J. Appl. Log. 7, No. 1, 3-25 (2009). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{M. Kaufmann} et al., J. Appl. Log. 7, No. 1, 3--25 (2009; Zbl 1183.68558) Full Text: DOI
Manolios, Panagiotis; Vroon, Daron Ordinal arithmetic: Algorithms and mechanization. (English) Zbl 1108.03020 J. Autom. Reasoning 34, No. 4, 387-423 (2005). MSC: 03B35 03E10 68T15 PDFBibTeX XMLCite \textit{P. Manolios} and \textit{D. Vroon}, J. Autom. Reasoning 34, No. 4, 387--423 (2005; Zbl 1108.03020) Full Text: DOI
Kaufmann, Matt; Moore, J. Strother Structured theory development for a mechanized logic. (English) Zbl 0971.03017 J. Autom. Reasoning 26, No. 2, 161-203 (2001). Reviewer: N.Ţăndăreanu (Craiova) MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{M. Kaufmann} and \textit{J. S. Moore}, J. Autom. Reasoning 26, No. 2, 161--203 (2001; Zbl 0971.03017) Full Text: DOI
Kaufmann, Matt Verification of Year 2000 conversion rules using the ACL2 theorem prover. (English) Zbl 1059.68588 Int. J. Softw. Tools Technol. Transf. 3, No. 1, 13-19 (2000). MSC: 68Q60 68T15 PDFBibTeX XML Full Text: DOI
Armando, Alessandro; Coglio, Alessandro; Giunchiglia, Fausto The control component of open mechanized reasoning systems. (English) Zbl 0958.68171 Armando, Alessandro (ed.) et al., Calculemus 99. Systems for integrated computation and deduction, Trento, Italy, July 11-12, 1999. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 23,3, 18 p., electronic only (1999). MSC: 68T35 68T15 PDFBibTeX XMLCite \textit{A. Armando} et al., in: Calculemus 99. Systems for integrated computation and deduction, Trento, Italy, July 11--12, 1999. Amsterdam: Elsevier. 18 p. (1999; Zbl 0958.68171)