[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> maths
[Index] || [Contents] || [Grades] Tue Aug 5 11:45:02 PDT 2003

Contents

    How I Write Formal Documents

     The Equation Editor in WordPerfect, MS Word, and AppleWorks has the special symbols needed for PC and LPC. It does not handle multicharacter variable well and the results our not portable.

    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

  1. ~dick/bin/mth2html name.mth Most can write
  2. Q name.mth instead. THe code is on the WWW: [ mth2html ]

    I use words for the operators in logic:

    [ logic_10_PC_LPC.html ]

    I express derivation rules using if of the Prolog:

  3. P :- Q1, Q2, Q3, ...

    I label propositions in my documents:

  4. (label): proposition.

    I prefix assumptions with "|-":

  5. |- (label): assumption.

    I show derivations like this

  6. (premises) |- (label): derived_proposition

    I use ".Let" to introduce assumptions and ".Close.Let" to unstack them:
    Let


    1. |- (label): Hypothesis
    2. derived_propositions
    3. ...

    (Close Let label)

    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.

Formulae and Definitions in Alphabetical Order