Physics Derivation Graph navigation Sign in

spectrum of formalized scientific documentation

Published 2021-08-07T23:03:00.002Z by Physics Derivation Graph

This post is an expansion of July 2020 post which was informed by Kaliszyk's survey.

Spectrum of formality:

category verbal natural language verbal presentation with aids written text semantic enrichment human-oriented controlled natural languages machine-oriented controlled natural languages computer algebra systems proof assistants, theorem provers
media human speaking human speaking; Latex containing text and equations -- BeamerLatex containing text and equations and hyperlinks Latex containing text and equations and hyperlinks;
mathematical physics: Physics Derivation Graph
SymPy Coq, Lean, Isabelle
purpose social knowledge transfer, one-to-one social knowledge transfer, one-to-many human readers; text search human readers; semantic search consistency validation of logical claims inference of novel knowledge correctness of inference rules; dimensional consistency; unit consistency mathematical correctness (consistency wrt a logical basis)
grouping standard practice knowledge representation mathematical correctness

manual annotation; supervised machine learning needs vocabulary and grammar:

Left side of the spectrum is less rigorous, right side is more rigorous. 

Left side of the spectrum has higher de Bruijn factor, right side has lower de Bruijn factor.

The Physics Derivation Graph is a machine-oriented controlled natural language that is integrated with a computer algebra system.

Semantic tagging can relate definitions for terms within a document to the associated variables used in that document. 
The motive for the semantic tagging is to enhance search-ability. Since search-ability doesn't benefit the author, the author is not motivated to do the work of tagging.

Semantic tagging can identify common words across documents in a corpus. OWL is interesting conceptually but since the author doesn't benefit, the author is not motivated to do the work of linking.