Published 2021-08-07T23:03:00.004Z 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 -- Beamer | Latex containing text and equations and hyperlinks | Latex containing text and equations and hyperlinks; sTex |
AIDA, ACE | text: RDF, OWL mathematical physics: Physics Derivation Graph math: ForTheL, Mizar |
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 | |||||
techniques | 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.