QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge

Authors

  • Michael Kohlhase Computer Science Jacobs University Bremen
  • Florian Rabe Computer Science Jacobs University Bremen

DOI:

https://doi.org/10.6092/issn.1972-5787/4570

Keywords:

QED, library integration, mathematical knoweldge management

Abstract

Proposed in 1994, the ``QED project'' was one of the seminally influential initiatives in automated reasoning: It envisioned the formalization of ``all of mathematics'' and the assembly of these formalizations in a single coherent database. Even though it never led to the concrete system, communal resource, or even joint research envisioned in the QED manifesto, the idea lives on and shapes the research agendas of a significant part of the community

This paper surveys a decade of work on representation languages and knowledge management tools for mathematical knowledge conducted in the KWARC research group at Jacobs University Bremen.
It assembles the various research strands into a coherent agenda for realizing the QED dream with modern insights and technologies.

Downloads

Published

2016-01-29

How to Cite

Kohlhase, M., & Rabe, F. (2016). QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. Journal of Formalized Reasoning, 9(1), 201–234. https://doi.org/10.6092/issn.1972-5787/4570

Issue

Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto

Section

QED 20th anniversary

License

Copyright (c) 2016 Michael Kohlhase, Florian Rabe

Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.

Creative Commons License

This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy