Meson Language Tutorial#
The nodes in Proofscape are linked together into proofs using a simple language called Meson. For example, the following Meson script:
A, so B, therefore C by D and E. Hence F, using G, so H.
produces the graph:
Meson is inspired by the Mizar language, which mimics the natural language used when proofs are written in English. Its name is meant to sound similar, while suggesting something small and light-weight.
This tutorial teaches the Meson language by example. Readers familiar with formal grammars may wish to also examine the Grammar, for a rigorous description of the language.
Contents