| Publication | Date of Publication | Type |
|---|
Reusing learning objects via theory morphisms
| 2024-12-04 | Paper |
Learning support systems based on mathematical knowledge management
Lecture Notes in Computer Science | 2024-02-28 | Paper |
Towards an annotation standard for STEM documents. Datasets, benchmarks, and spotters
Lecture Notes in Computer Science | 2024-02-28 | Paper |
scientific article; zbMATH DE number 7756106 (Why is no real title available?)
| 2023-10-27 | Paper |
Injecting formal mathematics into LaTeX
Lecture Notes in Computer Science | 2023-06-02 | Paper |
System description STEX3 -- a \LaTeX-based ecosystem for semantic/active mathematical documents
Lecture Notes in Computer Science | 2023-06-02 | Paper |
Logic-independent proof search in logical frameworks (short paper)
| 2022-11-09 | Paper |
Experiences from exporting major proof assistant libraries
Journal of Automated Reasoning | 2022-01-21 | Paper |
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
The Mathematical Intelligencer | 2021-04-19 | Paper |
Representing structural language features in formal meta-languages
| 2021-01-20 | Paper |
Towards a heterogeneous query language for mathematical knowledge
| 2021-01-20 | Paper |
FrameIT: detangling knowledge management from game design in serious games
| 2021-01-20 | Paper |
TGView3D: a system for 3-dimensional visualization of theory graphs
| 2021-01-20 | Paper |
Relational data across mathematical libraries
| 2020-01-22 | Paper |
Towards a unified mathematical data infrastructure: database and interface generation
| 2020-01-22 | Paper |
Integrating semantic mathematical documents and dynamic notebooks
| 2020-01-22 | Paper |
A mechanization of strong Kleene logic for partial functions
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Unification in an extensional lambda calculus with ordered function sorts and constant overloading
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
\(\Omega\)\textsc{mega}: towards a mathematical assistant
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
A colored version of the \(\lambda\)-calculus
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
QED reloaded: towards a pluralistic formal library of mathematical knowledge
| 2019-09-18 | Paper |
Virtual theories -- a uniform interface to mathematical knowledge bases
Mathematical Aspects of Computer and Information Sciences | 2019-03-14 | Paper |
Knowledge-based interoperability for mathematical software systems
Mathematical Aspects of Computer and Information Sciences | 2019-03-14 | Paper |
Translating the IMPS theory library to MMT/OMDoc
| 2018-10-18 | Paper |
Discourse phenomena in mathematical documents
| 2018-10-18 | Paper |
Automatically finding theory morphisms for knowledge management
| 2018-10-18 | Paper |
Knowledge amalgamation for computational science and engineering
| 2018-10-18 | Paper |
Theories as types
| 2018-10-18 | Paper |
Reasoning without believing: on the mechanisation of presuppositions and partiality
Journal of Applied Non-Classical Logics | 2018-08-28 | Paper |
Making PVS accessible to generic services by interpretation in a universal format
| 2018-01-04 | Paper |
Mathematical models as research data via flexiformal theory graphs
| 2017-07-21 | Paper |
Classification of alignments between concepts of formal mathematical systems
| 2017-07-21 | Paper |
Software citations, information systems, and beyond
| 2017-07-21 | Paper |
Visual structure in mathematical expressions
| 2017-07-21 | Paper |
The SMGloM Project and System: Towards a Terminology and Ontology for Mathematics
Mathematical Software – ICMS 2016 | 2016-09-28 | Paper |
Formula semantification and automated relation finding in the On-line Encyclopedia of Integer Sequences
Mathematical Software – ICMS 2016 | 2016-09-28 | Paper |
Interoperability in the OpenDreamKit project: the math-in-the-middle approach
Lecture Notes in Computer Science | 2016-08-30 | Paper |
Faceted search for mathematics
Mathematical Aspects of Computer and Information Sciences | 2016-05-25 | Paper |
A flexiformal model of knowledge dissemination and aggregation in mathematics
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Math Literate Knowledge Management via Induced Material
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Mathematical knowledge management: transcending the one-brain-barrier with theory graphs
European Mathematical Society Newsletter | 2015-01-02 | Paper |
Representing, archiving, and searching the space of mathematical knowledge
Mathematical Software – ICMS 2014 | 2014-09-08 | Paper |
Discourse-level parallel markup and meaning adoption in flexiformal theory graphs
Mathematical Software – ICMS 2014 | 2014-09-08 | Paper |
System description: a semantics-aware LaTeX-to-office converter
Lecture Notes in Computer Science | 2014-08-07 | Paper |
System description: MathHub.info
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Flexary operators for formalized mathematics
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Realms: a structure for consolidating knowledge about mathematical theories
Lecture Notes in Computer Science | 2014-08-07 | Paper |
A data model and encoding for a semantic, multilingual terminology of mathematics
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Mathematical formula search
European Mathematical Society Newsletter | 2014-01-21 | Paper |
A scalable module system
Information and Computation | 2014-01-10 | Paper |
A universal machine for biform theory graphs
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Semantics of \textsc{OpenMath} and \textsc{MathML3}
Mathematics in Computer Science | 2013-04-24 | Paper |
The Mizar Mathematical Library in OMDoc: translation and applications
Journal of Automated Reasoning | 2013-04-17 | Paper |
MathWebSearch 0.5: Scaling an Open Formula Search Engine
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Reimplementing the mathematics subject classification (MSC) as a linked open dataset
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Extending MKM formats at the statement level
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Semantic alliance: a framework for semantic allies
Lecture Notes in Computer Science | 2012-09-07 | Paper |
The Planetary project: towards eMath3.0
Lecture Notes in Computer Science | 2012-09-07 | Paper |
A proof theoretic interpretation of model theoretic hiding
Recent Trends in Algebraic Development Techniques | 2012-06-08 | Paper |
Towards logical frameworks in the heterogeneous tool set Hets
Recent Trends in Algebraic Development Techniques | 2012-06-08 | Paper |
Workflows for the management of change in science, technologies, engineering and mathematics
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Combining source, content, presentation, narration, and relational representation
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Project abstract: logic atlas and integrator (LATIN)
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Licensing the Mizar Mathematical Library (MML)
Lecture Notes in Computer Science | 2011-07-29 | Paper |
A foundational view on integration problems
Lecture Notes in Computer Science | 2011-07-29 | Paper |
The LaTeXML daemon: editable math on the collaborative web
Lecture Notes in Computer Science | 2011-07-29 | Paper |
scientific article; zbMATH DE number 5872255 (Why is no real title available?)
| 2011-03-30 | Paper |
Transforming large collections of scientific publications to XML
Mathematics in Computer Science | 2011-02-19 | Paper |
An Integrated Development Environment for Collections
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Towards MKM in the large: modular representation and scalable software architecture
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Dimensions of formality: a case study for MKM in software engineering
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Towards context-based disambiguation of mathematical expressions
| 2010-03-10 | Paper |
MathML-aware article conversion from LaTeX a comparison study
| 2009-10-26 | Paper |
Using La\TeX\ as a semantic markup format
Mathematics in Computer Science | 2009-09-18 | Paper |
Spreadsheet Interaction with Frames: Exploring a Mathematical Practice
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Unifying Math Ontologies: A Tale of Two Standards
Lecture Notes in Computer Science | 2009-07-09 | Paper |
A Mathematical Approach to Ontology Authoring and Documentation
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Compensating the Computational Bias of Spreadsheets with MKM Techniques
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Cut-Simulation and Impredicativity
Logical Methods in Computer Science | 2009-04-29 | Paper |
Cut-Simulation in Impredicative Logics
Automated Reasoning | 2009-03-12 | Paper |
Transforming the arχiv to XML
Lecture Notes in Computer Science | 2009-01-27 | Paper |
Notations for Living Mathematical Documents
Lecture Notes in Computer Science | 2009-01-27 | Paper |
A Search Engine for Mathematical Formulae
Artificial Intelligence and Symbolic Computation | 2009-01-15 | Paper |
Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Extended Formula Normalization for ε-Retrieval and Sharing of Mathematical Knowledge
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Communities of Practice in MKM: An Extensional Model
Lecture Notes in Computer Science | 2007-09-05 | Paper |
Capturing the Content of Physics: Systems, Observables, and Experiments
Lecture Notes in Computer Science | 2007-09-05 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Higher-order semantics and extensionality
Journal of Symbolic Logic | 2005-08-29 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
scientific article; zbMATH DE number 2090294 (Why is no real title available?)
| 2004-08-12 | Paper |
scientific article; zbMATH DE number 2090295 (Why is no real title available?)
| 2004-08-12 | Paper |
scientific article; zbMATH DE number 2079831 (Why is no real title available?)
| 2004-07-30 | Paper |
Resource-Adaptive Model Generation as a Performance Model
Logic Journal of the IGPL | 2004-03-07 | Paper |
Higher-Order Multi-Valued Resolution
Journal of Applied Non-Classical Logics | 2004-01-13 | Paper |
scientific article; zbMATH DE number 1951636 (Why is no real title available?)
| 2003-07-21 | Paper |
Communication protocols for mathematical services based on KQML and OMRS
| 2002-06-13 | Paper |
Formal representation issues in an open mathematical knowledge base. (Extended abstract)
| 2002-02-14 | Paper |
MBase: Representing knowledge and context for the integration of mathematical software systems
Journal of Symbolic Computation | 2002-01-02 | Paper |
scientific article; zbMATH DE number 1552534 (Why is no real title available?)
| 2001-10-30 | Paper |
scientific article; zbMATH DE number 1614716 (Why is no real title available?)
| 2001-07-05 | Paper |
scientific article; zbMATH DE number 1497743 (Why is no real title available?)
| 2001-03-06 | Paper |
scientific article; zbMATH DE number 1543304 (Why is no real title available?)
| 2001-02-27 | Paper |
Managing structural information by higher-order colored unification
Journal of Automated Reasoning | 2000-10-03 | Paper |
scientific article; zbMATH DE number 1303338 (Why is no real title available?)
| 2000-01-12 | Paper |
scientific article; zbMATH DE number 1324447 (Why is no real title available?)
| 1999-08-16 | Paper |
Integrating computer algebra into proof planning
Journal of Automated Reasoning | 1999-01-03 | Paper |
scientific article; zbMATH DE number 910746 (Why is no real title available?)
| 1996-07-28 | Paper |
