Kaliszyk, Cezary; Urban, Josef HOL(y)Hammer: online ATP service for HOL Light. (English) Zbl 1322.68177 Math. Comput. Sci. 9, No. 1, 5-22 (2015). MSC: 68T15 68T05 68T20 68T35 PDFBibTeX XMLCite \textit{C. Kaliszyk} and \textit{J. Urban}, Math. Comput. Sci. 9, No. 1, 5--22 (2015; Zbl 1322.68177) Full Text: DOI arXiv
Rowinska-Schwarzweller, Agnieszka; Schwarzweller, Christoph Towards mathematical knowledge management for electrical engineering. (English) Zbl 1202.68468 Kauers, Manuel (ed.) et al., Towards mechanized mathematical assistants. 14th symposium, Calculemus 2007, 6th international conference, MKM 2007, Hagenberg, Austria, June 27–30, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73083-5/pbk). Lecture Notes in Computer Science 4573. Lecture Notes in Artificial Intelligence, 371-380 (2007). MSC: 68U35 68T15 68T30 68T35 PDFBibTeX XMLCite \textit{A. Rowinska-Schwarzweller} and \textit{C. Schwarzweller}, Lect. Notes Comput. Sci. 4573, 371--380 (2007; Zbl 1202.68468) Full Text: DOI
Urban, Josef XML-izing Mizar: Making semantic processing and presentation of MML easy. (English) Zbl 1151.68681 Kohlhase, Michael (ed.), Mathematical knowledge management. 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005. Revised selected papers. Berlin: Springer (ISBN 3-540-31430-X/pbk). Lecture Notes in Computer Science 3863. Lecture Notes in Artificial Intelligence, 346-360 (2006). MSC: 68T35 68T15 68T30 PDFBibTeX XMLCite \textit{J. Urban}, Lect. Notes Comput. Sci. 3863, 346--360 (2006; Zbl 1151.68681) Full Text: DOI
Rudnicki, Piotr; Trybulec, Andrzej On the integrity of a repository of formalized mathematics. (English) Zbl 1022.68621 Asperti, Andrea (ed.) et al., Mathematical knowledge management. Second international conference, MKM 2003, Bertinoro, Italy, February 16-18, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2594, 162-174 (2003). MSC: 68T30 68T35 PDFBibTeX XMLCite \textit{P. Rudnicki} and \textit{A. Trybulec}, Lect. Notes Comput. Sci. 2594, 162--174 (2003; Zbl 1022.68621) Full Text: Link
Schwarzweller, Christoph Designing mathematical libraries based on requirements for theorems. (English) Zbl 1023.68130 Ann. Math. Artif. Intell. 38, No. 1-3, 193-209 (2003). MSC: 68W30 68T15 68T30 68T35 68N30 PDFBibTeX XMLCite \textit{C. Schwarzweller}, Ann. Math. Artif. Intell. 38, No. 1--3, 193--209 (2003; Zbl 1023.68130) Full Text: DOI