I have designed a formal ASCII based notation that can be used with formal methods. The idea was to have easy to type expressions and use translators to insert special symbols.
I use a simple ASCII editor (MS Notepad or vi for example). I use the extension ".mth" for such files. I have a UNIX tool that converts my notation into Web Pages using HTML and CSS. Any student on a CSci workstation or server can use this by the command
I use words for the operators in logic:
I express derivation rules using if of the Prolog:
I label propositions in my documents:
I prefix assumptions with "|-":
I show derivations like this
I use ".Let" to introduce assumptions and ".Close.Let" to unstack them:
I have listed the rules I follow in formal proofs in [ logic_2_Proofs.html ]
I have translated the text books rules: [ logic.html ]
For details see: [ intro_logic.html ] [ logic.html ] and [ http://ftp.csci.csusb.edu/dick/maths/ ] for more information.