This page is a survey of software related to the Physics Derivation Graph. For a literature review, see this page.
The scope of the Physics Derivation Graph does not include proof assistants (HOL, COQ, Lean) or formal proofs. No Category theory is used. The Physics Derivation Graph does not use Natural Language Processing. The Physics Derivation Graph is not intended as a tutorial.
The purpose of these efforts is to contrast with the scope and intention of the Physics Derivation Graph.
|Name and Website||Summary||Domain||Relation to PDG||Semantic Enrichment||Open source?||Free?||Active as of 2021-07-25?||Author or group|
|https://minireference.com/||PDF textbook for math and Physics||highschool and college math and Physics||concept maps||none||no||no||Ivan Savov|
|Road to Reality - https://reality.mentat.org/essays/reality/introduction||learn Physics using Lisp||physics equations as software||no||yes - https://github.com/mentat-collective/road-to-reality||yes||yes; see https://news.ycombinator.com/item?id=36005600||Sam Ritchie|
|SciLean - https://github.com/lecopivo/SciLean||"Framework for scientific computing such as solving differential equations, optimization or machine learning written in Lean."||SciLean is about computing things for science using Lean. Tomas started the project before mathlib4 was available, to mainly start thinking about how to use Lean for the practical aspects of scientific computing, with the understanding that formalization will come later. (By practical aspects, things like "how to numerically integrate an ODE"). Now that mathlib4 will be ported soon, SciLean will need to be rebuilt, for example, using mathlib's proper real numbers, rather than the reals defined ad hoc for the purposes of building SciLean.||formal verification of scientific computation||no||yes||yes||yes, as of 2023-06-19|
|SciLib - https://atomslab.github.io/LeanChemicalTheories/||Use Lean to prove science concepts||https://github.com/ATOMSLab/LeanChemicalTheories|
|Physics Derivation Graph||Goal: Create software that supports writing down all known mathematical physics in a way that can be both read by humans and checked by a computer algebra system.||Mathematical Physics||Yes||Yes||Yes||Yes||ben.is.located AT gmail.com|
|NIST Digital Library of Mathematical Functions||
In 1964 the National Institute of Standards and Technology published the Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables, edited by Milton Abramowitz and Irene A. Stegun.DLMF is the culmination of a project that was conceived in 1996 at NIST.
|Google's Knowledge Graph||Everything||PDG is also a knowledge graph||Yes||No||Yes||Yes|
|Langlands program||Summary||All of math?||None, other than scale of intent||No||No||Yes||Yes||mathematicians|
|Open Research Knowledge Graph||Computer Algebra System (CAS) in Python||Math, Physics||PDG relies on SymPy for validation of steps||No||Yes||Yes||Yes|
|System.com||Statistical relations between data (whereas wikidata is about semantic definitions and relationships). See comments and blog||Knowledge||None||No||Creative Commons Attribution ShareAlike License||Yes||as of 2022-03-15, yes|
|Evidence Algorithm||System for Automated Deduction (SAD) = automated processing of formal mathematical texts written in a special language called ForTheL (FORmal THEory Language) or in a traditional first-order language.||Math||Yes||Yes||Yes||Lyaletski, Verchinine, Paskevich|
|OntoMathPro||a Linked Data Hub for mathematics||Math||Yes||Yes; https://github.com/CLLKazan/OntoMathPro||Yes||Yes||Intelligent Search Systems and Semantic Technologies laboratory at Kazan Federal University|
|SysML Parametric Diagrams||Mathematical constraints and relations||Math||Identifies equations, parameters, and relations||No||Yes||Yes||Yes|
|QUDT - Quantities, Units, Dimensions and dataTypes||Ontology for units||Physics||PDG should use QUDT instead of a custom approach.||N/A||Yes||Yes||Yes|
|Semantic Web for Earth and Environmental Terminology (SWEET) Ontologies||SWEET is a highly modular ontology suite with ~6000 concepts in ~200 separate ontologies covering Earth system science. SWEET is a mid-level ontology and consists of nine top-level concepts that can be used as a foundation for domain-specific ontologies that extend these top-level SWEET components.||Science||No||Yes||Yes||Yes|
|zbMath Open||"zbMATH Open (formerly known as Zentralblatt MATH) is the world's most comprehensive and longest-running abstracting and reviewing service in pure and applied mathematics."||math search||No||Yes||Yes|
|Sophize||Knowledge graph for Math. There is no original content - it's all aggregated (and copied to the Sophize database) from sources like planetmath, metamath Wikipedia||Math||No||?||Yes||Yes||Abhishek Chugh|
|Nanopublications||Scientific claims in RDF||Science||No||Yes: https://github.com/Nanopublication/Guidelines||Yes||Yes||multiple|
|reasoning features for ACE texts and||Attempto Controlled English.
AIDA: a scheme for English sentences
|human-oriented controlled natural language||PDG is a machine-oriented CNL.||No||Yes||Yes||Yes||Tobias Kuhn|
|sTeX: Semantic Markup for LaTeX||sTeX system allows to embed /structural semantics into documents. Concretely sTeX is a “semantic version of LaTeX” that allows to use special macros to encode mathematical meaning explicitly.||Math||Yes||Yes||Yes||Yes||Knowledge Adaptation and Reasoning for Content|
|Naproche project (Natural language Proof Checking)||A central goal of Naproche is to develop a controlled natural language (CNL) for mathematical texts and adapted proof checking software which checks texts written in the CNL for syntactical and mathematical correctness.||Math||Yes||Yes||Yes|
|SnuggleTeX||Java library for converting fragments of LaTeX to XML (usually XHTML + MathML)||PDG could use MathML but does not currently.||Yes||Yes|
|PlanetPhysics||Physics||PDG is a collection of Physics knowledge||Yes||Yes||No|
|CmapTools||CMapTools knowledge modeling kit||Yes||Yes||Florida Institute for Human & Machine Cognition (IHMC)|
|MathDox formula editor||
a web-based editor for mathematical formulas.
Goal: "reconstruct mathematical vernacular in a computer-oriented environment."
Status: "a database which includes more than 9400 definitions of mathematical concepts and more than 49000 theorems."
|Wolfram Mathematical Functions||"World's largest collection of formulas and graphics about mathematical functions"||Math||Unknown||No||Yes||Yes||Stephen Wolfram|
|European Digital Mathematics Library||"EuDML makes the mathematics literature available online in the form of an enduring digital collection, developed and maintained by a network of institutions."||Math||Unknown||Yes|
|MioGatto annotation||A web-based annotation tool for Latex documents||Science||Yes||Yes||Yes||Yes|
|Incredible Proof Machine||
Similar in intent to the Physics Derivation Graph, though IPM is focused on logic.
I am impressed by the interface for drawing proofs.
The source code is available.
The source code
The comment thread on Hacker News
|Octopus||interview and discussion||Reproducible science||Focus on reproducibility||No||Yes||Yes||Yes|
|Math / Physics Problem Solver||The Math / Physics Problem Solver "solves simple math and physics problems stated in English."||Physics||No||Yes||Yes||Yes||Gordon Novak|
a tagging mechanism for words that is integrated with arXiv.
WISE stands for Web-based Interactive Semantic Environment.
|General Problem Solver||a computer program intended to work as a universal problem solver machine.||logic||similar in that starts with sources (axioms) and sinks (desired conclusions). The Physics Derivation Graph does not claim to enable automation of steps.||No||unknown||unknown||as SOAR|
|International Mathematical Knowledge Trust||Goal is to create "a comprehensive mathematical knowledge base."||Math||Unknown||Yes|
Authors are category theorists.
Goal is to "use natural language processing on a corpus of texts to assemble an imperfect but large and useful hierarchy of concepts" according to this thread. The "Plan is to start with things that can be done with existing natural language processing software."
|Murray-Rust Group at University of Cambridge||Software "for the representation, extraction and processing of scientific data across chemistry, materials science and solid-state physics. We're particularly interested in the following areas: chemical data representation and semantics, scientific publication and scientific literature, polymer informatics and materials informatics and simulation."||Chemistry, Material Science, Physics||Unknown||Yes||Yes||Yes||Murray-Rust Group|
|Crystallography Open Database||For an example, see https://www.crystallography.net/cod/1000118.html||Unknown||Yes||Yes||Yes|
|Numerical Atlas||A web-based seach interface for variables in arxiv papers.||Physics||Yes||Yes|
Input: web GUI for equations. Output: returns a list of equations similar to query. Each returned equation as the symbols defined.
Formula Database is a website described by the authors as a ``math search engine'' which has a built-in equation editor. The search feature is not just matching the \(\rm\LaTeX\) input -- it understands dot product and cross product. They have created a browser-based equation editor, similar to the equation editor in Microsoft Word. The search is of a backend database of content. The backend database of equations and symbols was manually entered by the project authors. A team of people have been working since about 2010 on this project. The data is stored as a high-dimensional graph. This project is not open source but access is currently free. A commercial launch is planned, though no date has been publicized. The objective is to allow students to search through literature. If you are a researcher, you might want to find whether the model already exists in literature. The grand view is that formula-database will serve as a universal reference for equations.
Formula Database was founded in 2012 by a group of students and researchers at UW-Madison. The idea originated three years prior, when one of our founders, then an undergraduate, was frustrated at the difficulty in finding the correct formula he needed to solve his engineering homework. This challenge has been leveraged into creating an innovative search engine to allow individuals to search for formulas based upon either their contents or mathematical structure. Formula Database lets users input measurable parameters—such as mass, distance, or time—and get equations that provide a relation between these items. Alternatively, using the Equation Editor, users can write a mathematical equation exactly as they would on a whiteboard or paper and discover information about the formula’s use and purpose. Currently we are developing the completed product to allow users to enjoy this functionality. We anticipate launching for a beta test at the end of August 2012.
Gather all knowledge in a text-based structure with hyperlinks.
In contrast, the Physics Derivation Graph is effectively language-independent.
An interface for putting expressions into a graph format. Inference rules and feeds were
not included, nor is checking of the graph via a computer algebra system.
The website EquationMap (http://equationmap.com; site not currently available) is an interface for derivations, focused primarily on mathematics. There is no backend database of content; instead content is dynamically generated by the user. Equations are manually entered using \LaTeX syntax and the graph of the derivation can be visualized using the same interface. The content is not open source and access is currently free. This is close to what the GUI for the Physics Derivation Graph is intended to behave like, with the exception that EquationMap doesn't include the concept of atomic inference rules.
|Mathematical Physics||No||No; proprietary||Yes||No|
|SymboLab||A web interface for solving symbolic expressions. There is no graph. There is a backend database of content.||Math, Physics||Probably?||No||Yes||No|
A static set of linked concept maps for topics in Physics.
Concept maps are linked to text, graphs, and equations.
Although hyperlinked concept maps are a departure from the standard textbook presentation of physics,
the leaves of this tree are the same content found in textbooks.
similar to Wikipediain that
it is text based for edges.
|Physics||No||The licensing of the content is described as "not freeware or shareware" by the author, though the site is free to access.||Yes||Yes||Carl R. (Rod) Nave|
|Wolfram Mathematica||A computer algebra system, whereas the Physics Derivation Graph is documentation of known mathematical physics relations.||Math, Physics||No||No||No||Yes||Stephen Wolfram|
|Wolfram Physics||Uses graphs as a method of developing fundemental Physics concepts.
Completely unrelated to the Physics Derivation Graph.
For a useful overview and assessment, listen to Episode 155 of Sean Carrl's Mindscape
All science knowledge with a searchable web interface.
Wolfram Alpha has a backend database of content which is not open source; access is a mix of free and paid.
The closest to the Physics Derivation Graph is step-by-step solver
|Science||Probably?||No||mixture; step-by-step is $4.75/month as of 2021-08-08||Yes||Stephen Wolfram|
OpenMath is an extensible standard for representing the semantics of mathematical objects.https://en.wikipedia.org/wiki/OpenMath
|Math||Yes||Yes||Yes||Yes||Knowledge Adaptation and Reasoning for Content|
PhysML is part of the OMdoc effort.
PhysML is for identifying categories of content.
PhysML is distinct from http://sciencewise.info/ in that ScienceWise is about linking specific terms to a common database, whereas PhysML is for identifying categories of content.
|Physics||Yes||Knowledge Adaptation and Reasoning for Content|
"Both MathML and OpenMath address mathematical formulas in isolation, whereas OMDoc allows to express the structure of mathematical documents, for example the relation between definitions, theorems and proofs."(source: "Extracting Mathematical Semantics from LATEX Documents")
|Math||Yes||Knowledge Adaptation and Reasoning for Content|
See also Ajit Narayanan: A word game to communicate in any language which is about the app FreeSpeech.
|knowledge management||no||unknown||unknown||yes||Andries van Renssen|
Presentation MathML (layout only) and Content MathML (semantics)
|Math, Mathematical Physics||Yes||Yes||Yes||Yes|
LatexML converts to Presentation MathML, not Content MathML
LaTeXML 2012 - A Year of LaTeXML
Strategies for Parallel Markup
|Math, Mathematical Physics||Yes||Yes||Bruce Miller|
|Formal Mathematical Language||a modeling and documentation language for mathematics.
the FMathL system might turn into a user-friendly automatic mathematical assistant for retrieving, editing, and checking mathematics (but also computer science and theoretical physics) in both informal, partially formalized, and completely formalized mathematical form.
"Digital Scientific Notations as a Human-Computer Interface in Computer-Aided Research"
"Leibniz is a subset of Maude with different syntax"
"Scientific notations for the digital era"
|Science||Yes?||Yes: CRAPL||Yes||Yes||Konrad Hinsen|
A "group blog" with the intent of
hosting "polymath" projects – massively collaborative mathematical research projects.
Polymath projects are massively collaborative mathematical research programs, in which a single problem, group of problems, or other mathematical task is worked on by a large group of mathematicians.
The Physics Derivation Graph is an effort to create the software infrastructure for a "PolyPhysics"
Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. The site has a collection of web pages generated from those proofs and lets you see mathematics developed in complete detail from first principles, with absolute rigor.
|directed graphs in linguistics||Examples include visuwords.com and synonym||Linguistics||varies||varies||varies||varies|
MathLingua is a language for easily creating a collection of mathematical knowledge, including definitions, theorems, axioms, and conjectures. ... The goal is to allow one to express mathematical concepts in a higher level language that focuses on what a statement means instead of how it is represented in a logical framework.
|Math||Yes?||Yes: Apache 2.0||Yes||Yes|
|Atlas IDE||IDE for math. Includes visualization. Automatic linking of variables. Variables have definitions.||Mathematical Physics||Yes||No||No||Yes|
|calcula.tech IDE||Create Latex equations in a web browser and solve numerical equations.
|blockpad.net||mash-up of MathCAD and Excel in a web browser||Math||No||No||Yes|