visualization of step validation; 271 steps to address

I created a page listing all the steps from every derivation. The utility is that I can summarize how many steps are valid (180 out of 638, or 28%), how many are declarations and assumptions (179+8, or 29%), and how many fail or are not checked -- the remaining 40%.

My plan is to work on addressing the
638-(180+179+8)=271 
failed or unchecked expressions.

I expect SymPy doesn't support all the inference rules, so I need a way to categorize that issue.

linear representation of a directed graph

A derivation typically does not show all steps. The steps of a derivation are typically not linear.

  Figure 1: left side is a directed acyclic graph where some nodes are hidden and each node can be linearly ordered. In the center all nodes have been shown in a linear presentation. On the right, all nodes in a non-linear display.

a web-based GUI for drawing graphs with latex

Back in 2014 the EquationMap interface featured the ability enter latex into nodes and create graphs with edges.



Similar web interfaces for drawing graphs include

• https://github.com/neyric/wireit and https://github.com/neyric/webhookit (both no longer supported)
• Cytoscape.js; see https://pathwaycommons.github.io/cytoscape-sbgn-stylesheet/
• https://modeling-languages.com/javascript-drawing-libraries-diagrams/

However, none of these support rendering Latex or Mathjax

My current approach of generating PNG images from Latex and then rendering the PNGs as a graph using d3.js seems to work sufficiently well. I could modify the interface such that the existing webform is on the same page as the rendered graph.

The user would select an inference rule, provide the expressions, and render the graph all in a single page.
What isn't clear in my mental model is how to connect edges to new steps. 

Increasing levels of formality in a trivial physics statement

In this post I start with a trivial observation about Physics concepts and attempt to add layers of formalization through semantic enrichment. Inspired by sTeX, I use pseudo-Latex which has no supported implementation. RDF tags might be more appropriate.

The initial observation is

The relation between period, T, and linear frequency, f, is T = 1/f. Thus frequency as a function of period is f = 1/T.

The purpose of using this as a starting point is that it is simple and easily understood by a human.
The rest of this post explores what semantic additions would be needed for a computer to parse the text.

Each of these transitions can be identified manually. I don't have reliable ways of automating this process.

*********************
The first change is conversion from ASCII to Latex, a common presentation method in Math and Physics. This change only alters presentation. I've highlighted the changes in red.

The relation between period, $T$, and linear frequency, $f$, is
\begin{equation}
T = 1/f.
\end{equation}
Thus frequency as a function of period is
\begin{equation}
f = 1/T.
\end{equation}

*********************

The next change is to bound claims being made.

\claim{1}{The relation between period, $T$, and linear frequency, $f$, is
  \begin{equation}
    T = 1/f.
  \end{equation}
}
Thus \claim{2}{frequency as a function of period is
  \begin{equation}
    f = 1/T.
  \end{equation}
}

*********************

Replace "thus" with the relation between claims.

\claim{1}{The relation between period, $T$, and linear frequency, $f$, is
  \begin{equation}
    T = 1/f.
  \end{equation}
}
\relation_between_claims{claim 2 is derivable from claim 1}
\claim{2}{frequency as a function of period is
  \begin{equation}
    f = 1/T.
  \end{equation}
}

*********************

Within each claim there are variables and symbols. Identify those.
I've inserted parenthesis to make the order of operations clear.

\claim{1}{The relation between \named_variable{period}, \symbol{T}, and \named_variable{linear frequency}, \symbol{f}, is
  \begin{equation}
    \symbol{T} \operator{=} (\integer{1}\operator{/}\symbol{f}).
  \end{equation}
}
\relation_between_claims{claim 2 is derivable from claim 1}
\claim{2}{The \named_variable{frequency} as a function of \named_variable{period} is
  \begin{equation}
    \symbol{f} \operator{=} (\integer{1}\operator{/}\symbol{T}).
  \end{equation}
}

Visually, this could be represented by color-coded boxing

Here claims are red, connections are light green, expressions are dark green, named variables are pink, variables are blue, operators are light blue, and operators are purple.

This visualization seems to relate to discourse representation theory (DRT) though I don't know how to leverage it. See box notation here and here.


*********************
The "T" and "f" symbols are conventions that are used in other papers. We can indicate that by assigning universal identifiers.
Similarly, the operators "/" and "=" are defined in other papers. Those also get a universal ID.
The relation between named variables and symbols needs to be made explicit.
With those associations made, replace the symbols and operators in the expressions.

\def{symbol{T} = pdg2948}                   % the symbol "T" has a (universal) Godel number
\def{symbol{f} = pdg9215}                   % the symbol "f" has a (universal) Godel number
\def{operator{/} = pdg1340}                 % the operator "/" has a (universal) Godel number
\def{operator{=} = pdg8821}                 % the operator "=" has a (universal) Godel number
\def{named_variable{period} = symbol{T}}    % the named variable "period" is equivalent to the symbol "T"
\def{named_variable{frequency} = symbol{f}} % the named variable "frequency" is equivalent to the symbol "f"

\claim{1}{The relation between \named_variable{period}, pdg2948, and \named_variable{linear frequency}, pdg9215, is
  \begin{equation}
    pdg2948 pdg8821 (\integer{1} pdg1340 pdg9215).
  \end{equation}
}
\relation_between_claims{claim 2 is derivable from claim 1}
\claim{2}{The \named_variable{frequency} as a function of \named_variable{period} is
  \begin{equation}
    pdg9215 pdg8821 (\integer{1} pdg1340 pdg2948).
  \end{equation}
}

One of the purposes of associating a symbol "T" with a universal identifier is that the type can be specified. Here "f" and "T" are both Real valued.

At this point the relation between claims 1 and 2 could be converted to SymPy and verified; see
https://derivationmap.net/review_derivation/884319/

graph visualization isn't a requirement for the Physics Derivation Graph

The central concept of the Physics Derivation Graph is that there are mathematical links between expressions. This means that navigating the content can be intuitively done using a graph. However, navigating a graph visually doesn't scale well.

The Physics Derivation Graph doesn't have to be presented as a graph. A derivation is typically presented in a linear format.

Storing the content of the Physics Derivation Graph does not require a graph storage database.