Comparison of the Physics Derivation Graph with other projects
This page is a survey of software related to the Physics Derivation Graph.
For a literature review, see this page.
The scope of this survey is any project that recognizes underlying structure in Physics (beyond narrative text and equations).
The purpose of this survey is to contrast other efforts with the scope and intention of the Physics Derivation Graph.
"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.
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.
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.
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.
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.
"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."
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
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.
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.
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."
"EuDML makes the mathematics literature available online in the form of an enduring digital collection, developed and maintained by a network of institutions."
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.
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."
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."
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.
Below are a few screenshots from the Internet Archive.
Frontpage of the FormulaDatabase.
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.
Screenshot of the EquationMap website. The input mechanism is not shown because this screenshot is from the Internet Archive.
Screenshot of the option to provide .tex files to EquationMap website, and download .tex files.
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.
HyperPhysics is
similar to Wikipediain that
it is text based for edges. HyperPhysics has
what appears to be a graph (hand drawn), but is actually a multi-level
tree -- a concept diagram. For example, content in
the Classical Mechanics subpage
does not link to any other subject.
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.
"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."
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.
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.
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.
Frontpage of the FormulaDatabase.
Categories of data in the FormulaDatabase.
Objects in the FormulaDatabase.
Screenshot of the EquationMap website. The input mechanism is not shown because this screenshot is from the Internet Archive.
Screenshot of the option to provide .tex files to EquationMap website, and download .tex files.