Kohlhase, Michael; Rabe, Florian Experiences from exporting major proof assistant libraries. (English) Zbl 07461271 J. Autom. Reasoning 65, No. 8, 1265-1298 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Kohlhase} and \textit{F. Rabe}, J. Autom. Reasoning 65, No. 8, 1265--1298 (2021; Zbl 07461271) Full Text: DOI arXiv
Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. (English) Zbl 1493.68391 Math. Intell. 43, No. 1, 78-87 (2021). Reviewer: Truong Hoang Le (Hanoi) MSC: 68Vxx 00A30 00A35 01A65 01A67 PDFBibTeX XMLCite \textit{J. Carette} et al., Math. Intell. 43, No. 1, 78--87 (2021; Zbl 1493.68391) Full Text: DOI
Kohlhase, Michael; Rabe, Florian; Wenzel, Makarius Making Isabelle content accessible in knowledge representation formats. (English) Zbl 07756106 Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 1, 24 p. (2020). MSC: 03B70 68N30 PDFBibTeX XMLCite \textit{M. Kohlhase} et al., LIPIcs -- Leibniz Int. Proc. Inform. 175, Article 1, 24 p. (2020; Zbl 07756106) Full Text: DOI arXiv
Kohlhase, Michael; Rabe, Florian; Sacerdoti Coen, Claudio; Schaefer, Jan Frederik Logic-independent proof search in logical frameworks (short paper). (English) Zbl 07614524 Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12166, 395-401 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Kohlhase} et al., Lect. Notes Comput. Sci. 12166, 395--401 (2020; Zbl 07614524) Full Text: DOI
Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian Making PVS accessible to generic services by interpretation in a universal format. (English) Zbl 1484.68311 Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 319-335 (2017). MSC: 68V15 68V20 68V30 PDFBibTeX XMLCite \textit{M. Kohlhase} et al., Lect. Notes Comput. Sci. 10499, 319--335 (2017; Zbl 1484.68311) Full Text: DOI
Rabe, Florian Morphism axioms. (English) Zbl 1373.03132 Theor. Comput. Sci. 691, 55-80 (2017). Reviewer: Ernst-Erich Doberkat (Dortmund) MSC: 03G30 68Q65 PDFBibTeX XMLCite \textit{F. Rabe}, Theor. Comput. Sci. 691, 55--80 (2017; Zbl 1373.03132) Full Text: DOI
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian Classification of alignments between concepts of formal mathematical systems. (English) Zbl 1367.68309 Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 83-98 (2017). MSC: 68T30 68T15 68U35 PDFBibTeX XMLCite \textit{D. Müller} et al., Lect. Notes Comput. Sci. 10383, 83--98 (2017; Zbl 1367.68309) Full Text: DOI Link
Rabe, Florian The future of logic: foundation-independence. (English) Zbl 1436.03179 Log. Univers. 10, No. 1, 1-20 (2016). MSC: 03B70 03B22 03B16 PDFBibTeX XMLCite \textit{F. Rabe}, Log. Univers. 10, No. 1, 1--20 (2016; Zbl 1436.03179) Full Text: DOI
Rabe, Florian Lax theory morphisms. (English) Zbl 1367.03061 ACM Trans. Comput. Log. 17, No. 1, Article No. 5, 36 p. (2015). MSC: 03B70 PDFBibTeX XMLCite \textit{F. Rabe}, ACM Trans. Comput. Log. 17, No. 1, Article No. 5, 36 p. (2015; Zbl 1367.03061) Full Text: DOI
Horozal, Fulya; Rabe, Florian Formal logic definitions for interchange languages. (English) Zbl 1417.68206 Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 171-186 (2015). MSC: 68T30 68T27 68U15 PDFBibTeX XMLCite \textit{F. Horozal} and \textit{F. Rabe}, Lect. Notes Comput. Sci. 9150, 171--186 (2015; Zbl 1417.68206) Full Text: DOI
Kaliszyk, Cezary; Rabe, Florian Towards knowledge management for HOL Light. (English) Zbl 1304.68158 Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 357-372 (2014). MSC: 68T15 68T30 PDFBibTeX XMLCite \textit{C. Kaliszyk} and \textit{F. Rabe}, Lect. Notes Comput. Sci. 8543, 357--372 (2014; Zbl 1304.68158) Full Text: DOI
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael Flexary operators for formalized mathematics. (English) Zbl 1304.68171 Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 312-327 (2014). MSC: 68T30 PDFBibTeX XMLCite \textit{F. Horozal} et al., Lect. Notes Comput. Sci. 8543, 312--327 (2014; Zbl 1304.68171) Full Text: DOI
Rabe, Florian; Kohlhase, Michael A scalable module system. (English) Zbl 1358.68283 Inf. Comput. 230, 1-54 (2013). MSC: 68T30 68T27 PDFBibTeX XMLCite \textit{F. Rabe} and \textit{M. Kohlhase}, Inf. Comput. 230, 1--54 (2013; Zbl 1358.68283) Full Text: DOI
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina Towards logical frameworks in the heterogeneous tool set Hets. (English) Zbl 1278.68286 Mossakowski, Till (ed.) et al., Recent trends in algebraic development techniques. 20th international workshop, WADT 2010, Etelsen, Germany, July 1–4, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-28411-3/pbk). Lecture Notes in Computer Science 7137, 139-159 (2012). MSC: 68T27 03B40 68Q65 68T15 PDFBibTeX XMLCite \textit{M. Codescu} et al., Lect. Notes Comput. Sci. 7137, 139--159 (2012; Zbl 1278.68286) Full Text: DOI
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian A proof theoretic interpretation of model theoretic hiding. (English) Zbl 1278.68202 Mossakowski, Till (ed.) et al., Recent trends in algebraic development techniques. 20th international workshop, WADT 2010, Etelsen, Germany, July 1–4, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-28411-3/pbk). Lecture Notes in Computer Science 7137, 118-138 (2012). MSC: 68Q65 03B40 68T15 PDFBibTeX XMLCite \textit{M. Codescu} et al., Lect. Notes Comput. Sci. 7137, 118--138 (2012; Zbl 1278.68202) Full Text: DOI
Horozal, Fulya; Rabe, Florian Representing model theory in a type-theoretical logical framework. (English) Zbl 1236.03027 Theor. Comput. Sci. 412, No. 37, 4919-4945 (2011). MSC: 03B70 03B10 03C98 68T15 PDFBibTeX XMLCite \textit{F. Horozal} and \textit{F. Rabe}, Theor. Comput. Sci. 412, No. 37, 4919--4945 (2011; Zbl 1236.03027) Full Text: DOI
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio A foundational view on integration problems. (English) Zbl 1278.68289 Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 107-122 (2011). MSC: 68T27 68T15 68T30 68W30 PDFBibTeX XMLCite \textit{F. Rabe} et al., Lect. Notes Comput. Sci. 6824, 107--122 (2011; Zbl 1278.68289) Full Text: DOI arXiv
Horozal, Fulya; Rabe, Florian Representing model theory in a type-theoretical logical framework. (English) Zbl 1291.03068 Ayala-Rincón, Mauricio (ed.) et al., Proceedings of the fourth workshop on logical and semantic frameworks, with applications (LSFA 2009), Brasilia, Brazil, August 28, 2009. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 256, 49-65 (2009). MSC: 03B70 03B10 03C99 PDFBibTeX XMLCite \textit{F. Horozal} and \textit{F. Rabe}, Electron. Notes Theor. Comput. Sci. 256, 49--65 (2009; Zbl 1291.03068) Full Text: DOI
Sojakova, Kristina; Rabe, Florian Translating a dependently-typed logic to first-order logic. (English) Zbl 1253.03100 Corradini, Andrea (ed.) et al., Recent trends in algebraic development techniques. 19th international workshop, WADT 2008, Pisa, Italy, June 13–16, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03428-2/pbk). Lecture Notes in Computer Science 5486, 326-341 (2009). MSC: 03G30 68Q65 PDFBibTeX XMLCite \textit{K. Sojakova} and \textit{F. Rabe}, Lect. Notes Comput. Sci. 5486, 326--341 (2009; Zbl 1253.03100) Full Text: DOI
Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff THF0 – the core of the TPTP language for higher-order logic. (English) Zbl 1165.68447 Armando, Alessandro (ed.) et al., Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Berlin: Springer (ISBN 978-3-540-71069-1/pbk). Lecture Notes in Computer Science 5195. Lecture Notes in Artificial Intelligence, 491-506 (2008). MSC: 68T15 PDFBibTeX XMLCite \textit{C. Benzmüller} et al., Lect. Notes Comput. Sci. 5195, 491--506 (2008; Zbl 1165.68447) Full Text: DOI