Prof. Dr. Michael Kohlhase
Department of Informatics, Knowledge Representation/Processing (Computer Science)
Adjunct associate professor for Computer Science at Carnegie Mellon University
Friedrich-Alexander-Universität Erlangen-Nürnberg
michael.kohlhase@fau.de
See my profile at FAU
Knowledge representation for STEM (Science, Technology, Engineering, Mathematics), Inference-based techniques for natural language processing, Computer-supported education and user assitance, Research data management, Mathematical knowledge, inference, computation, language, and examples as data
FAU MoD Lecture: Prospects of formalized Mathematics (November 2, 2023)
Publications
2024
Guided Tours in ALeA: Assembling Tailored Educational Dialogues from Semantically Annotated Learning Objects
International Workshops of the 26th European Conference on Artificial Intelligence, ECAI 2023 (Kraków, POL, September 30, 2023 - October 4, 2023)
In: Sławomir Nowaczyk, Przemysław Biecek, Neo Christopher Chung, Mauro Vallati, Paweł Skruch, Joanna Jaworek-Korjakowska, Simon Parkinson, Alexandros Nikitas, Martin Atzmüller, Tomáš Kliegr, Ute Schmid, Szymon Bobek, Nada Lavrac, Marieke Peeters, Roland van Dierendonck, Saskia Robben, Eunika Mercier-Laurent, Gülgün Kayakutlu, Mieczyslaw Lech Owoc, Karl Mason, Abdul Wahid, Pierangela Bruno, Francesco Calimeri, Francesco Cauteruccio, Giorgio Terracina, Diedrich Wolter, Jochen L. Leidner, Michael Kohlhase, Vania Dimitrova (ed.): Communications in Computer and Information Science 2024
DOI: 10.1007/978-3-031-50485-3_39 , , :
Project VoLL-KI: Learning from Learners
In: Künstliche Intelligenz (2024)
ISSN: 0933-1875
DOI: 10.1007/s13218-024-00846-9 , , , , , , , , , , , :
Reusing Learning Objects via Theory Morphisms
17th International Conference on Intelligent Computer Mathematics, CICM 2024 (Montreal, QC, CAN, August 5, 2024 - August 9, 2024)
In: Andrea Kohlhase, Laura Kovács (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2024
DOI: 10.1007/978-3-031-66997-2_10 , :
Term Extraction for Domain Modeling
22. Fachtagung Bildungstechnologien (DELFI) (Fulda, September 9, 2024 - September 11, 2024)
In: Gesellschaft für Informatik e.V. (ed.): Proceedings of the 22. Fachtagung Bildungstechnologien (DELFI) 2024 , , , , , :
2023
Learning Support Systems based on Mathematical Knowledge Management
16th Conference on Intelligent Computer Mathematics (CICM 2023) (Cambridge, September 4, 2023 - September 8, 2023)
In: Lecture Notes in Computer Science, Cham: 2023 , , , , , :
Learning with ALeA: Tailored experiences through annotated course material
Workshop KI-Bildung (Berlin, September 28, 2023 - September 28, 2023)
In: Maike Klein, Daniel Krupka, Cornelia Winter, Volker Wohlgemuth (ed.): INFORMATIK 2023. Designing Futures: Zukünfte gestalten, Bonn: 2023
URL: https://nextcloud.gi.de/s/Y28MkNMjGnE2JY9 , , , , , :
The Y-Model - Formalization of Computer-Science Tasks in the Context of Adaptive Learning Systems
IEEE German Education Conference (GeCon) (Berlin, August 2, 2023 - August 4, 2023)
DOI: 10.1109/GECon58119.2023.10295148 , , , , :
The Potential of Answer Classes in Large-scale Written Computer-Science Exams
Hochschuldidaktik Informatik (HDI) 2021 (Aachen, September 13, 2023 - September 14, 2023) , , , :
Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters
Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023 (Cambridge, GBR, September 5, 2023 - September 8, 2023)
In: Catherine Dubois, Manfred Kerber (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2023
DOI: 10.1007/978-3-031-42753-4_13 , :
2022
System Description STEX3-A LATEX-Based Ecosystem for Semantic/Active Mathematical Documents
15th International Conference on Intelligent Computer Mathematics (CICM) part of the Computational Logic Autumn Summit (CLAS) (Tbilisi)
In: INTELLIGENT COMPUTER MATHEMATICS, CICM 2022, CHAM: 2022
DOI: 10.1007/978-3-031-16681-5_13 , :
Injecting Formal Mathematics Into LATEX
15th International Conference on Intelligent Computer Mathematics (CICM) part of the Computational Logic Autumn Summit (CLAS) (Tbilisi)
In: INTELLIGENT COMPUTER MATHEMATICS, CICM 2022, CHAM: 2022
DOI: 10.1007/978-3-031-16681-5_12 , :
2021
Mathematical Information Retrieval
In: Tetsuya Sakai, Douglas W. Oard, Noriko Kando (ed.): Evaluating Information Retrieval and Access Tasks, Singapore: Springer Nature, 2021, p. 169-185 (Information Retrieval Series, Vol.43)
ISBN: 978-981-15-5554-1
DOI: 10.1007/978-981-15-5554-1_12 , :
Experiences from Exporting Major Proof Assistant Libraries
In: Journal of Automated Reasoning (2021)
ISSN: 0168-7433
DOI: 10.1007/s10817-021-09604-0 , :
2020
(Deep) FAIR mathematics
In: it - Information Technology (2020)
ISSN: 1611-2776
DOI: 10.1515/itit-2019-0028 , , :
Towards a heterogeneous query language for mathematical knowledge
13th International Conference on Intelligent Computer Mathematics, CICM 2020 (Bertinoro, July 26, 2020 - July 31, 2020)
In: Christoph Benzmüller, Bruce Miller (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
DOI: 10.1007/978-3-030-53518-6_3 , , :
Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge
In: Mathematical Intelligencer (2020)
ISSN: 0343-6993
DOI: 10.1007/s00283-020-10006-0 , , , :
FrameIT: Detangling Knowledge Management from Game Design in Serious Games
The 13th Conference on Intelligent Computer Mathematics (CICM 2020) (Bertinoro, July 26, 2020 - July 31, 2020)
In: Springer (ed.): Lecture Notes in Computer Science, vol 12236 2020
DOI: 10.1007/978-3-030-53518-6_11 , , , , , , , :
Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
10th International Joint Conference on Automated Reasoning, IJCAR 2020 (Virtual, Online, July 1, 2020 - July 4, 2020)
In: Nicolas Peltier, Viorica Sofronie-Stokkermans (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
DOI: 10.1007/978-3-030-51074-9_22 , , , :
Making Isabelle Content Accessible in Knowledge Representation Formats
25th International Conference on Types for Proofs and Programs, TYPES 2019 (Oslo, June 11, 2019 - June 14, 2019)
In: Marc Bezem, Assia Mahboubi, Assia Mahboubi (ed.): Leibniz International Proceedings in Informatics, LIPIcs 2020
DOI: 10.4230/LIPIcs.TYPES.2019.1 , , :
Tgview3d: A system for 3-dimensional visualization of theory graphs
13th International Conference on Intelligent Computer Mathematics, CICM 2020 (Bertinoro, July 26, 2020 - July 31, 2020)
In: Christoph Benzmüller, Bruce Miller (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
DOI: 10.1007/978-3-030-53518-6_20 , , :
Representing Structural Language Features in Formal Meta-languages
The 13th Conference on Intelligent Computer Mathematics (CICM 2020) (Bertinoro, July 26, 2020 - July 31, 2020)
In: Springer (ed.): Lecture Notes in Computer Science, vol 12236 2020
DOI: 10.1007/978-3-030-53518-6_13 , , , :
Context graphs for legal reasoning and argumentation
3rd International Workshop on Systems and Algorithms for Formal Argumentation, SAFA 2020 (Virtual, Online, September 8, 2020)
In: Sarah A. Gaggl, Matthias Thimm, Mauro Vallati (ed.): CEUR Workshop Proceedings 2020 , , :
Prototyping Controlled Mathematical Languages in Jupyter Notebooks
7th International Congress on Mathematical Software, ICMS 2020 (Braunschweig, DEU, July 13, 2020 - July 16, 2020)
In: Anna Maria Bigatti, Jacques Carette, James H. Davenport, Michael Joswig, Timo de Wolff (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
DOI: 10.1007/978-3-030-52200-1_40 , , :
GLIF: A Declarative Framework for Symbolic Natural Language Understanding
6th Workshop on Formal and Cognitive Reasoning, FCR 2020 (, September 22, 2020)
In: Christoph Beierle, Marco Ragni, Frieder Stolzenburg, Matthias Thimm (ed.): CEUR Workshop Proceedings 2020 , :
2019
Integrating Semantic Mathematical Documents and Dynamic Notebooks
12th International Conference on Intelligent Computer Mathematics, CICM 2019 (Prague, July 8, 2019 - July 12, 2019)
In: Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2019
DOI: 10.1007/978-3-030-23250-4_19 , , , :
Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation
12th International Conference on Intelligent Computer Mathematics, CICM 2019 (Prague, July 8, 2019 - July 12, 2019)
In: Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2019
DOI: 10.1007/978-3-030-23250-4_3 , , :
Relational Data Across Mathematical Libraries
12th International Conference on Intelligent Computer Mathematics, CICM 2019 (Prague, July 8, 2019 - July 12, 2019)
In: Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2019
DOI: 10.1007/978-3-030-23250-4_5 , , , , , :
2018
Discourse phenomena in mathematical documents
11th International Conference on Intelligent Computer Mathematics, CICM 2018
DOI: 10.1007/978-3-319-96812-4_14 , , :
Towards context graphs for argumentation logics
2018 Conference "Learning, Knowledge, Data, Analytics", LWDA 2018
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85053594694&origin=inward :
Translating the IMPS theory library to MMT/OMDoc
11th International Conference on Intelligent Computer Mathematics, CICM 2018
DOI: 10.1007/978-3-319-96812-4_2 , :
Translating the IMPS theory library to MMT/OMDoc
11th International Conference on Intelligent Computer Mathematics, CICM 2018
DOI: 10.1007/978-3-319-96812-4_2 , :
Discourse phenomena in mathematical documents
11th International Conference on Intelligent Computer Mathematics, CICM 2018
DOI: 10.1007/978-3-319-96812-4_14 , , :
A proposal for an OpenMath JSON encoding
Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation, CME-EI 2018, Formal Mathematics for Mathematicians, FMM 2018, Computer Algebra in the Age of Types, CAAT 2018, Formal Verification of Physical Systems, FVPS 2018, Mathematical Models and Mathematical Software as Research Data 2018, M3SRD 2018 and 29th OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS 2018
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85060579045&origin=inward , :
Model pathway diagrams for the representation of mathematical models
In: Optical and Quantum Electronics 50 (2018), Article No.: ARTN 70
ISSN: 0306-8919
DOI: 10.1007/s11082-018-1321-7 , , , , :
Automatically finding theory morphisms for knowledge management
11th International Conference on Intelligent Computer Mathematics, CICM 2018
DOI: 10.1007/978-3-319-96812-4_18 , , :
Theories as Types
9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
DOI: 10.1007/978-3-319-94205-6_38 , , :
Knowledge amalgamation for computational science and engineering
11th International Conference on Intelligent Computer Mathematics, CICM 2018
DOI: 10.1007/978-3-319-96812-4_20 , , :
Syntactic/semantic analysis for high-precision math linguistics
Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation, CME-EI 2018, Formal Mathematics for Mathematicians, FMM 2018, Computer Algebra in the Age of Types, CAAT 2018, Formal Verification of Physical Systems, FVPS 2018, Mathematical Models and Mathematical Software as Research Data 2018, M3SRD 2018 and 29th OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS 2018
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85060658105&origin=inward , :
A proposal for an openMath JSON encoding
Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation, CME-EI 2018, Formal Mathematics for Mathematicians, FMM 2018, Computer Algebra in the Age of Types, CAAT 2018, Formal Verification of Physical Systems, FVPS 2018, Mathematical Models and Mathematical Software as Research Data 2018, M3SRD 2018 and 29th OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS 2018
In: Proceedings of the Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation 2018
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85060579045∨igin=inward , :
2017
A standard for aligning mathematical concepts
2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85018973947&origin=inward , , , :
Math object identifiers - Towards research data in mathematics
Lernen, Wissen, Daten, Analyse - 2017 Learning. Knowledge. Data. Analytics, LWDA 2017 (Rostock)
In: Lernen, Wissen, Daten, Analyse - 2017 Learning. Knowledge. Data. Analytics, LWDA 2017 2017
URL: https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85030126012&origin=inward :- Toloaca I., Kohlhase M.:
Notation-based semantification
MathUI 2016
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85018973557∨igin=inward
Visual structure in mathematical expressions
10th International Conference on Intelligent Computer Mathematics, CICM 2017
DOI: 10.1007/978-3-319-62075-6_15 , , :
Mathematical models as research data via flexiformal theory graphs
In: 10th International Conference on Intelligent Computer Mathematics, CICM 2017 2017
DOI: 10.1007/978-3-319-62075-6_16 , , , :
Making PVS accessible to generic services by interpretation in a universal format
8th International Conference on Interactive Theorem Proving, ITP 2017
DOI: 10.1007/978-3-319-66107-0_21 , , , :
Knowledge-Based Interoperability for Mathematical Software Systems
In: Johannes Blömer and Temur Kutsia and Dimitris Simos (ed.): MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences 2017 , , , , , , :
Classification of alignments between concepts of formal mathematical systems
10th International Conference on Intelligent Computer Mathematics, CICM 2017
In: 10th International Conference on Intelligent Computer Mathematics, CICM 2017 2017
DOI: 10.1007/978-3-319-62075-6_7 , , , , :
FrameIT reloaded: Serious math games from modular math ontologies
2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016
In: 2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016 2017 , , :
Software citations, information systems, and beyond
10th International Conference on Intelligent Computer Mathematics, CICM 2017
DOI: 10.1007/978-3-319-62075-6_8 , :- Kohlhase M., De Feo L., Müller D., Pfeiffer M., Rabe F., Thiéry N., Vasilyev V., Wiesing T.:
Knowledge-based interoperability for mathematical software systems
7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
DOI: 10.1007/978-3-319-72453-9_14
Mathematical models as research data in numerical simulation of opto-electronic devices
17th International Conference on Numerical Simulation of Optoelectronic Devices, NUSOD 2017
DOI: 10.1109/NUSOD.2017.8010073 , , , :
A Flexible, Interactive Theory-Graph Viewer
CICM 2017 , , :
Virtual theories – A uniform interface to mathematical knowledge bases
7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
DOI: 10.1007/978-3-319-72453-9_17 , , :
Virtual theories – A uniform interface to mathematical knowledge bases
7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
DOI: 10.1007/978-3-319-72453-9_17 , , :
Virtual Theories -- A Uniform Interface to Mathematical Knowledge Bases
7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
In: Johannes Blömer and Temur Kutsia and Dimitris Simos (ed.): MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences 2017
DOI: 10.1007/978-3-319-72453-9_17 , , , :
2016
- Ginev D., Iancu M., Jucovshi C., Kohlhase A., Kohlhase M., Oripov A., Schefter J., Sperber W., Teschke O., Wiesing T.:
The SMGloM project and system: Towards a terminology and ontology for mathematics
Springer Verlag, 2016
ISBN: 9783319424316
DOI: 10.1007/978-3-319-42432-3_58
Faceted search for mathematics
6th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2015
DOI: 10.1007/978-3-319-32859-1_35 , :
QED reloaded: Towards a pluralistic formal library of mathematical knowledge
In: Journal of Formalized Reasoning 9 (2016), p. 201-234
ISSN: 1972-5787
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84957079748&origin=inward , :
Formula semantification and automated relation finding in the on-line encyclopedia for integer sequences
5th International Conference on Mathematical Software, ICMS 2016
DOI: 10.1007/978-3-319-42432-3_60 , :
Interoperability in the OpenDreamKit project: The math-in-the-middle approach
9th International Conference on Intelligent Computer Mathematics, CICM 2016
DOI: 10.1007/978-3-319-42547-4_9 , , , , , , , , , :
2015
Faceted search for mathematics
Learning, Knowledge, Adaptation Workshops, LWA 2015: Knowledge Discovery, Data Mining and Machine Learning, KDML 2015, Knowledge Management, FGWM 2015, Information Retrieval, IR 2015 and Database Systems, FGDB 2015
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84944340107&origin=inward , :
A flexiformal model of knowledge dissemination and aggregation in mathematics
International Conference on Intelligent Computer Mathematics, CICM 2015
DOI: 10.1007/978-3-319-20615-8_9 , :
Math literate knowledge management via induced material
International Conference on Intelligent Computer Mathematics, CICM 2015
DOI: 10.1007/978-3-319-20615-8_12 , :- Kohlhase A., Kohlhase M., Guseva A.:
Context in spreadsheet comprehension
2nd Workshop on Software Engineering Methods in Spreadsheets, SEMS 2015, Co-located with the 37th International Conference on Software Engineering, ICSE 2015
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84930355041&origin=inward
Importing the OEIS library into OMDoc
Learning, Knowledge, Adaptation Workshops, LWA 2015: Knowledge Discovery, Data Mining and Machine Learning, KDML 2015, Knowledge Management, FGWM 2015, Information Retrieval, IR 2015 and Database Systems, FGDB 2015
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84944342791&origin=inward , , :
Assessment for spreadsheets
2nd Workshop on Software Engineering Methods in Spreadsheets, SEMS 2015, Co-located with the 37th International Conference on Software Engineering, ICSE 2015
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84930336641&origin=inward , , :
2014
Open math map: Interaction
Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924891544&origin=inward , :
Towards Ontological Support for Principle Solutions in Mechanical Engineering
8th International Conference on Formal Ontology in Information Systems (Rio de Janeiro)
In: 8th International Conference on Formal Ontology in Information Systems 2014
DOI: 10.3233/978-1-61499-438-1-427 , , , , , :
Semantic Support for Engineering Design Processes
13th International Design Conference, DESIGN 2014 (Dubrovnik)
In: In Proc. 13th International Design Conference, DESIGN 2014 2014
URL: https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=84924387161&origin=inward , , , , , :
Realms: A structure for consolidating knowledge about mathematical theories
2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
DOI: 10.1007/978-3-319-08434-3_19 , , :
Flexary operators for formalized mathematics
2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
DOI: 10.1007/978-3-319-08434-3_23 , , :
System description: MathHub.info
2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
DOI: 10.1007/978-3-319-08434-3_33 , , , :
Representing, archiving, and searching the space of mathematical knowledge
4th International Congress on Mathematical Software, ICMS 2014 (Seoul)
DOI: 10.1007/978-3-662-44199-2_5 , , :
System description: A semantics-aware LATEX-to-office converter
2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
DOI: 10.1007/978-3-319-08434-3_35 , :
A data model and encoding for a semantic, multilingual terminology of mathematics
2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
DOI: 10.1007/978-3-319-08434-3_13 :
Extension proposal: Records in pragmatic open math
Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924891647&origin=inward :
OpenMath language extensions
Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924873356&origin=inward :
Discourse-level parallel markup and meaning adoption in flexiformal theory graphs
4th International Congress on Mathematical Software, ICMS 2014 (Seoul)
DOI: 10.1007/978-3-662-44199-2_7 , :
2013
OpenMathMap: Accessing Math via Interactive Maps
Joint Workshops of the 8th Workshop on Mathematical User Interfaces, MathUI 2013, 25th OpenMath Workshop, OpenMath 2013, 5th International Workshop on Programming Languages for Mechanised Mathematical Systems, PLMMS 2013 and the 2nd International Workshop on Theorem Proving Components for Educational Software, ThEdu 2013 and Work in Progress at Conference on Intelligent Computer Mathematics, CICM 2013
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924872163&origin=inward , :
The Mizar mathematical library in OMDoc: Translation and applications
In: Journal of Automated Reasoning 50 (2013), p. 191-202
ISSN: 0168-7433
DOI: 10.1007/s10817-012-9271-4 , , , :
Full semantic transparency: Overcoming boundaries of applications
14th IFIP TC 13 International Conference on Human-Computer Interaction, INTERACT 2013 (Cape Town)
DOI: 10.1007/978-3-642-40477-1_25 , , , :
A universal machine for biform theory graphs
Conference on Intelligent Computer Mathematics, CICM 2013, Co-located with the MKM 2013, Calculemus 2013, DML 2013, and Systems and Projects 2013 (Bath)
DOI: 10.1007/978-3-642-39320-4_6 , , :
Mashups using mathematical knowledge: Why formulas are different
In: Brigitte Endres-Niggemeyer (ed.): Semantic Mashups: Intelligent Reuse of Web Resources, Springer Berlin Heidelberg, 2013, p. 171-204
ISBN: 9783642364020
DOI: 10.1007/978-3-642-36403-7_6 , :
A scalable module system
In: Information and Computation 230 (2013), p. 1-54
ISSN: 0890-5401
DOI: 10.1016/j.ic.2013.06.001 , :
2012
A proof theoretic interpretation of model theoretic hiding
20th International Workshop on Algebraic Development Techniques, WADT 2010 (Etelsen)
DOI: 10.1007/978-3-642-28412-0_9 , , , , :
Towards logical frameworks in the heterogeneous tool set hets
20th International Workshop on Algebraic Development Techniques, WADT 2010 (Etelsen)
DOI: 10.1007/978-3-642-28412-0_10 , , , , , :
Semantic alliance: A framework for semantic allies
Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
DOI: 10.1007/978-3-642-31374-5_4 , , , :
Extending MKM formats at the statement level
Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
DOI: 10.1007/978-3-642-31374-5_5 , , :
Reasoning without believing: On the mechanisation of presuppositions and partiality
In: Journal of Applied Non-Classical Logics 22 (2012), p. 295-317
ISSN: 1166-3081
DOI: 10.1080/11663081.2012.705962 , :
The flexiformalist manifesto
14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012 (Timisoara)
DOI: 10.1109/SYNASC.2012.78 :
The Planetary project: Towards eMath3.0
Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
DOI: 10.1007/978-3-642-31374-5_34 :
MathWebSearch 0.5: Scaling an open formula search engine
Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
DOI: 10.1007/978-3-642-31374-5_23 , , :
Semantics of OpenMath and MathML3
In: Mathematics in Computer Science 6 (2012), p. 235-260
ISSN: 1661-8270
DOI: 10.1007/s11786-012-0113-x , :- Lange C., Ion P., Dimou A., Bratsas C., Sperber W., Kohlhase M., Antoniou I.:
Bringing mathematics to the web of data: The case of the mathematics subject classification
9th Extended Semantic Web Conference, ESWC 2012 (Heraklion, Crete)
DOI: 10.1007/978-3-642-30284-8_58
2011
- Autexier S., David C., Dietrich D., Kohlhase M., Zholudev V.:
Workflows for the management of change in science, technologies, engineering and mathematics
18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
DOI: 10.1007/978-3-642-22673-1_12
Project abstract: Logic atlas and integrator (LATIN)
18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
DOI: 10.1007/978-3-642-22673-1_24 , , , , :- David C., Ginev D., Kohlhase M., Matican B., Mirea S.:
A framework for semantic publishing of modular content objects
1st Workshop on Semantic Publishing 2011, SePublica 2011 - Co-located with the 8th Extended Semantic Web Conference, ESWC 2011 (Hersonissos, Crete)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84890730016&origin=inward
The LaTeXML daemon: Editable math on the collaborative web
Symposium on Learning, Knowledge, and Adaptivity 2011, LWA 2011 (Magdeburg)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874005493&origin=inward , , , :
Combining source, content, presentation, narration, and relational representation
18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
DOI: 10.1007/978-3-642-22673-1_15 , , , , :
Maintaining islands of consistency via versioned links
29th ACM International Conference on Design of Communication, SIGDOC'11 (Pisa)
DOI: 10.1145/2038476.2038510 , :- Wolska M., Grigore M., Kohlhase M.:
Using discourse context to interpret object-denoting mathematical expressions
4th Workshop Towards a Digital Mathematics Library, DML 2011
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84870532306&origin=inward - Kohlhase M., Corneli J., David C., Ginev D., Jucovschi C., Kohlhasea A., Lange C., Matican B., Mirea S., Zholudev V.:
The planetary system: Web 3.0 & active documents for STEM
11th International Conference on Computational Science, ICCS 2011 (Singapore)
DOI: 10.1016/j.procs.2011.04.063
Towards a flexible notion of document context
29th ACM International Conference on Design of Communication, SIGDOC'11 (Pisa)
DOI: 10.1145/2038476.2038512 , :- Alama J., Kohlhase M., Mamane L., Naumowicz A., Rudnicki P., Urban J.:
Licensing the Mizar mathematical library
18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
DOI: 10.1007/978-3-642-22673-1_11 - Lange C., Kohlhase M., David C., Ginev D., Kohlhase A., Matican B., Mirea S., Zholudev V.:
The planetary system: Executable science, technology, engineering and math papers
8th Extended Semantic Web Conference, ESWC 2011 (Heraklion, Crete)
DOI: 10.1007/978-3-642-21064-8_37
Mathwebsearch 0.5 an open formula search engine
Symposium on Learning, Knowledge, and Adaptivity 2011, LWA 2011 (Magdeburg)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874016713&origin=inward , :
A foundational view on integration problems
18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
DOI: 10.1007/978-3-642-22673-1_8 , , :
2010
- David C., Kohlhase M., Lange C., Rabe F., Zhiltsov N., Zholudev V.:
Publishing math lecture notes as linked data
7th Extended Semantic Web Conference, ESWC 2010 (Heraklion, Crete)
DOI: 10.1007/978-3-642-13489-0_26
STEXIDE: An integrated development environment for STEX collections
10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010 (Paris)
DOI: 10.1007/978-3-642-14128-7_29 , :
Dimensions of formality: A case study for MKM in software engineering
10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010 (Paris)
DOI: 10.1007/978-3-642-14128-7_31 , , :- Kohlhase A., Kohlhase M., Lange C.:
STEX+: A system for flexible formalization of linked data
6th International Conference on Semantic Systems, I-SEMANTICS '10 (Graz)
DOI: 10.1145/1839707.1839712
Towards MKM in the large: Modular representation and scalable software architecture
10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010 (Paris)
DOI: 10.1007/978-3-642-14128-7_32 , , :
Scripting documents with XQuery: Virtual documents in TNTBase
Balisage: The Markup Conference 2010 (Montreal, QC)
DOI: 10.4242/BalisageVol5.Zholudev01 , :- Dumitrache A., Lange C., Kohlhase M., Aschenbeck N.:
Prototyping a browser for a listed buildings database* with semantic MediaWiki
5th Workshop on Semantic Wikis - Linking Data and People, SemWiki 2010 - 7th Extended Semantic Web Conference, ESWC 2010 (Hersonissos, Heraklion, Crete)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84873471498&origin=inward
Transforming large collections of scientific publications to XML
In: Mathematics in Computer Science 3 (2010), p. 299-307
ISSN: 1661-8270
DOI: 10.1007/s11786-010-0024-7 , , , , :
2009
Unifying math ontologies: A tale of two standards
16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
DOI: 10.1007/978-3-642-02614-0_23 , :
An architecture for linguistic and semantic analysis on the ARXMLIV corpus
39th Jahrestagung der Gesellschaft fur Informatik e.V. (GI): Im Focus das Leben, INFORMATIK 2009 39th Annual Meeting of the German Informatics Society (GI): Focus on Life, INFORMATIK 2009 (Lubeck)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874316647&origin=inward , , , , , :
Compensating the computational bias of spreadsheets with MKM techniques
16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
DOI: 10.1007/978-3-642-02614-0_29 , :
Modeling task experience in user assistance systems
27th ACM International Conference on Design of Communication, SIGDOC'09 (Bloomington, IN)
DOI: 10.1145/1621995.1622021 , :
Spreadsheet interaction with frames: Exploring a mathematical practice
16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
DOI: 10.1007/978-3-642-02614-0_28 , :
Cut-simulation and impredicativity
In: Logical Methods in Computer Science 5 (2009), p. 1-21
ISSN: 1860-5974
DOI: 10.2168/LMCS-5(1:6)2009 , , :
Semantic transparency in user assistance systems
27th ACM International Conference on Design of Communication, SIGDOC'09 (Bloomington, IN)
DOI: 10.1145/1621995.1622013 , :
What you understand is what you get: Assessment in spreadsheets
LWA 2009 - Workshop-Woche: Lernen-Wissen-Adaptivitat - Learning, Knowledge and Adaptivity (Darmstadt)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874134110&origin=inward , :
A mathematical approach to ontology authoring and documentation
LWA 2009 - Workshop-Woche: Lernen-Wissen-Adaptivitat - Learning, Knowledge and Adaptivity (Darmstadt)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874182293&origin=inward , :- Kohlhase M., Lemburg J., Schröder L., Schulz E.:
Formal management of CAD/CAM processes
2nd World Congress on Formal Methods, FM 2009 (Eindhoven)
DOI: 10.1007/978-3-642-05089-3_15
TNTBase: Versioned storage for XML
Balisage: The Markup Conference 2009 (Montreal, QC)
DOI: 10.4242/BalisageVol3.Zholudev01 , :
A mathematical approach to ontology authoring and documentation
16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
DOI: 10.1007/978-3-642-02614-0_31 , :
Context-aware adaptation: A case study on mathematical notations
In: Information Systems Management 26 (2009), p. 215-230
ISSN: 1058-0530
DOI: 10.1080/10580530903017583 , :- Stamerjohanns H., Ginev D., David C., Misev D., Zamdzhiev V., Kohlhase M.:
MathML-aware article conversion from LATEX a comparison study
2nd Workshop on Towards a Digital Mathematics Library, DML 2009 (Grand Bend, ON)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84896692132&origin=inward
Applying semantic techniques to search and analyze bug tracking data
In: Journal of Network and Systems Management 17 (2009), p. 285-308
ISSN: 1064-7570
DOI: 10.1007/s10922-009-9134-4 , , , , :
2008
Using LATEX as a semantic markup format
In: Mathematics in Computer Science 2 (2008), p. 279-304
ISSN: 1661-8270
DOI: 10.1007/s11786-008-0055-5 :
Semantic knowledge management for education
In: Proceedings of the IEEE 96 (2008), p. 970-989
ISSN: 0018-9219
DOI: 10.1109/JPROC.2008.921606 , :
SWiM: A semantic wiki for mathematical knowledge management
In: 1st Workshop on Semantic Wikis 2008
DOI: 10.4018/978-1-59904-877-2.ch004 , :
Notations for living mathematical documents
9th Int. Conf. Artificial Intelligence and Symbolic Computation, AISC 2008 - 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008 - 7th Int. Conf. Mathematical Knowledge Management, MKM 2008 (Birmingham)
DOI: 10.1007/978-3-540-85110-3_41 , , :
Towards a community of practice toolkit based on semantically marked up artifacts
1st World Summit on the Knowledge Society, WSKS 2008 (Athens)
DOI: 10.1007/978-3-540-87781-3_5 , :
An exchange format for modular knowledge
LPAR 2008 Workshops on Knowledge Exchange: Automated Provers and Proof Assistants, KEAPPA 2008 and the 7th International Workshop on the Implementation of Logics, IWIL 2008 (Doha)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84885598893&origin=inward , :
Transforming the arχiv to XML
9th Int. Conf. Artificial Intelligence and Symbolic Computation, AISC 2008 - 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008 - 7th Int. Conf. Mathematical Knowledge Management, MKM 2008 (Birmingham)
DOI: 10.1007/978-3-540-85110-3_46 , :
2007
Lecture Notes in Comuter Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes: Preface
29th Annual German Conference on Artificial Intelligence (KI 2006) (Bremen)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-35448943067&origin=inward , , :
Reexamining the MKM value proposition: From math web search to math web research
14th Symposium on Calculemus 2007 and 6th International Conference on Mathematical Knowledge Management, MKM 2007 (Hagenberg)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-38049042760&origin=inward , :
Managing variants in document content and narrative structures
Workshop on Learning, Knowledge, and Adaptivity, LWA 2007 (Halle)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84869721576&origin=inward , , :
Panta rhei
Workshop on Learning, Knowledge, and Adaptivity, LWA 2007 (Halle)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874010902&origin=inward , :
Extended formula normalization for e-retrieval and sharing of mathematical knowledge
14th Symposium on Calculemus 2007 and 6th International Conference on Mathematical Knowledge Management, MKM 2007 (Hagenberg)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-38049028250&origin=inward , :
2006
Capturing the content of physics: Systems, observables, and experiments
5th International Conference on Mathematical Knowledge Management, MKM 2006 (Wokingham)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749546748&origin=inward , , :
An exploration in the space of mathematical knowledge , :
Communities of practice in MKM: An extensional model
5th International Conference on Mathematical Knowledge Management, MKM 2006 (Wokingham)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749542803&origin=inward , :
OMDoc - An open markup format for mathematical documents [version 1.2]
2006 :- Benzmüller C., Brown C., Kohlhase M.:
Cut-simulation in impredicative logics
Third International Joint Conference on Automated Reasoning, IJCAR 2006 (Seattle, WA)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749556449&origin=inward
A semantic wiki for mathematical knowledge management
1st Workshop on Semantic Wikis - From Wiki to Semantics, SemWiki 2006 - Co-located with the ESWC 2006 (Budva)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84873470933&origin=inward , :
A search engine for mathematical formulae
8th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2006 (Beijing)
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749635061&origin=inward , :
2004
Higher-order semantics and extensionality
In: Journal of Symbolic Logic 69 (2004), p. 1027-1088
ISSN: 0022-4812
DOI: 10.2178/jsl/1102022211 , , :
CPOINT: Dissolving the author's dilemma
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-35048892955&origin=inward , :
2003
Towards collaborative content management and version control for structured mathematical knowledge , :
Resource-adaptive model generation as a performance model
In: Logic Journal of the Igpl 11 (2003), p. 435-456
ISSN: 1367-0751 , :
2002
- Siekmann J., Benzmüller C., Brezhnev V., Cheikhrouhou L., Fiedler A., Franke A., Horacek H., Kohlhase M., Meier A., Melis E., Moschner M., Normann I., Pollet M., Sorge V., Ullrich C., Wirth C., Zimmer J.:
Proof development with Ωmega
18th International Conference on Automated Deduction, CADE 2002
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84948980176&origin=inward
System description: The mathweb software bus for distributed mathematical reasoning
18th International Conference on Automated Deduction, CADE 2002
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84948958841&origin=inward , :
2001
- Kohlhase M., Franke A.:
MBase: Representing knowledge and context for the integration of mathematical software systems
In: Journal of Symbolic Computation 32 (2001), p. 365-402
ISSN: 0747-7171
DOI: 10.1006/jsco.2000.0468
OMDoc: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge
5th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2000
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84974687882&origin=inward :
Communication Protocols for mathematical services based on KQML and OMRS , , :
2000
ICoS-2 Inference in Computational Semantics. Workshop Proceedings
2000 , (ed.):
System description: MBASE, an open mathematical knowledge base
17th International Conference on Automated Deduction, CADE 2000
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84937429345&origin=inward , :
Managing structural information by higher-order colored unification
In: Journal of Automated Reasoning 25 (2000), p. 123-164
ISSN: 0168-7433
DOI: 10.1023/A:1006282725324 , :
Model generation for discourse representation theory
In: Werner Horn (ed.): Proceedings of of the 14th European Conference on Artifical Intelligence 2000 :
Feature logic for dotted types: A formalism for complex word meanings
In: Proceedings of the 38th Annual Meeting of the Association for Computational Linguistics 2000 , :
1999
System description: MathWeb, an agent-based communication layer for distributed automated theorem proving
16th International Conference on Automated Deduction, CADE 1999
DOI: 10.1007/3-540-48660-7_17 , :- Franke A., Hess S., Jung C., Kohlhase M., Sorge V.:
Agent-oriented integration of distributed mathematical services
In: Journal of Universal Computer Science 5 (1999), p. 156-187
ISSN: 0958-695X
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-0001536634&origin=inward - Siekmann J., Hess S., Benzmüller C., Cheikhrouhou L., Fiedler A., Horacek H., Kohlhase M., Konrad K., Meier A., Melis E., Pollet M., Sorge V.:
ℒΩUI: ℒovely ΩMEGA User Interface
In: Formal Aspects of Computing 11 (1999), p. 326-342
ISSN: 0934-5043
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-0345829693&origin=inward
MBase: Representing mathematical knowledge in a relational data base
In: Electronic Notes in Theoretical Computer Science 23 (1999), p. 451-468
ISSN: 1571-0661
DOI: 10.1016/S1571-0661(05)80615-2 , :
Higher-order multi-valued resolution
In: Journal of Applied Non-Classical Logics 9 (1999), p. 455-477
ISSN: 1166-3081
DOI: 10.1080/11663081.1999.10510980 , :
1998
Extensional higher-order resolution
15th International Conference on Automated Deduction, CADE 1998
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84858341103&origin=inward , :
Integrating Computer Algebra into Proof Planning
In: Journal of Automated Reasoning 21 (1998), p. 327-355
ISSN: 0168-7433
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-0032287894&origin=inward , , :
System description: Leo— A higher-order theorem prover
15th International Conference on Automated Deduction, CADE 1998
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84872799915&origin=inward , :
1997
- Benzmuller C, Cheikhrouhou L, Fehrer D, Fiedler A, Huang XR, Kerber M, Kohlhase M, Konrad K, Meier A, Melis E, Schaarschmidt W, Siekmann J, Sorge V:
Omega MEGA: Towards a mathematical assistant - Benzmüller C., Cheikhrouhou L., Fehrer D., Fiedler A., Huang X., Kerber M., Kohlhase M., Konrad K., Meier A., Melis E., Schaarschmidt W., Siekmann J., Sorge V.:
ΩMEGA: Towards a mathematical assistant
14th International Conference on Automated Deduction, CADE 1997
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84860987429&origin=inward
A colored version of the λ-calculus
14th International Conference on Automated Deduction, CADE 1997
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-35048867096&origin=inward , :
Computing parallelism in discourse
In: Martha E. Pollack (ed.): Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI) 1997 , :
1996
Corrections and higher-order unification , , :- Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.:
The proof development environment Ω-MKRP
In: Informatik - Forschung und Entwicklung 11 (1996), p. 20-26
ISSN: 0178-3564
DOI: 10.1007/s004500050036
Integrating computer algebra with proof planning
4th International Symposium on Design and Implementation of Symbolic Computation Systems, DISCO 1996
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-21444434314&origin=inward , , :
1995
Higher-order tableaux
4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, TABLEAUX 1995
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84949190517&origin=inward :
1994
- Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.:
Keim: A toolkit for automated deduction
12th International Conference on Automated Deduction, CADE-12 1994
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84943317064&origin=inward - Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.:
Ω-MKRP: A proof development environment
12th International Conference on Automated Deduction, CADE-12 1994
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84961346097&origin=inward
Adapting methods to novel tasks in proof planning
18th Annual German Conference on Artificial Intelligence, KI 1994
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-2342658424&origin=inward , , , :
A mechanization of strong Kleene logic for partial functions
12th International Conference on Automated Deduction, CADE-12 1994
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84956993662&origin=inward , :- Johann P., Kohlhase M.:
Unification in an extensional lambda calculus with ordered function sorts and constant overloading
12th International Conference on Automated Deduction, CADE-12 1994
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84945308194&origin=inward
Unification in a sorted λ-calculus with term declarations and function sorts
18th Annual German Conference on Artificial Intelligence, KI 1994
URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85028712606&origin=inward :
1993
UNIFICATION IN A LAMBDA-CALCULUS WITH INTERSECTION TYPES
In: Proceedings of the International Logic Programming Symposion ILPS'93 1993 , :
1992
Unification in order-sorted type theory
International Conference on Logic Programming and Automated Reasoning, LPAR 1992
DOI: 10.1007/BFb0013080 :
You might like!
• Our FAU MoD Community
• About us
• FAU MoD Lecture Series
• Upcoming events
FAU MoD Lecture
Date: TBA Event: FAU MoD Lecture Organized by: FAU MoD, the Research Center for Mathematics of Data at Friedrich-Alexander-Universität Erlangen-Nürnberg ...
FAU MoD Lecture: Do you think you understand sex and death? Why predictions about biological processes require more than just intuition
Date: Tue. January 28, 2025 Event: FAU MoD Lecture Organized by: FAU MoD, the Research Center for Mathematics of Data ...
FAU MoD Lecture
Date: Thu. December 05, 2024 Event: FAU MoD Lecture Organized by: FAU MoD, the Research Center for Mathematics of Data ...