2^ndTetrapod Workshop: Interoperable Knowledge Representation

4 September 2023

at CICM 2023

The Tetrapod model organizes mathematical knowledge into 4+1 aspects, visualized as the corners and the center of a tetrahedral shape. The corners represent fundamentally different ways of assigning semantics, each with an ecosystem of highly specialized tools and large libraries:

• Inference: proofs, especially if formalized and mechanically verified in proof assistants
• Computation: algorithms, especially if executably implemented in programming languages and computer algebra systems
• Tabulation: systematic lists of examples, especially if encoded as concrete objects stored in databases
• Documentation: human-readable narrative explanations, especially if systematically structured and annotated to enable machince processing
A key novelty of the model is to identify as the central aspect the intersection of the above.
• Ontology: names, types, definitions, notations, and properties of mathematical objects
This aspect is usually not made explicit in mathematical software but is critical for knowledge exchange between them.

Program

After a first installation at FLoC 2018, this workshop will revisit all issues pertaining to mathematical knowledge, with a particular focus on modularity and aspect-integration.
The workshop will be informal and discussion-oriented. Depending on the interest of the participants, the program may be improvised.
Informal suggestions of discussion topics, presentations, demos, or problem sessions on any related topic are very welcome.
Please email suggestions to tetrapod at lists.informatik.uni-erlangen.de.

• 14:00: Michael Kohlhase, Aspects of Mathematical Knowledge
  This talk will give a brief introduction to the Tetrapod model and then transition into free discussion.
  Slides
• 15:00: Natarajan Shankar, Modularity in Mathematical Knowledge
  This talk will update on the 2018 presentation aiming at inducing lively discussion.
  Slides
• 16:00: Coffee break
• 16:30: Catherine Dubois, Interoperability through Isomorphisms
  This talk will present technical results on bridging across formalizations.
  Slides
• 17:15: Panel discussion on the Mathematical Software of the Future
  Based on the issues raised in the previous talks, we speculate on how we should design the cross-aspect, modular, interoperable mathematical software systems of the future.
  Tentative list of attendants:
  • All above speakers
  • William Farmer
  • Lawrence Paulson
  Moderation: Florian Rabe
The times above are estimates, and we will freely deviate based on the course of the discussions.

Organizers

• Katja Bercic
• William Farmer
• Michael Kohlhase
• Dennis Müller
• Florian Rabe