# Calculational proofs and notations

What is a calculational solution, or a calculational proof, or an equational solution, or an equational proof? For now I'll simply point you to 'A Logical Approach to Discrete Math'.

## Notations

I use the notations from the above-mentioned book, with the following ASCII-zations:
• Universal and existential quantification is written as A and E.
• Equivalence is written as ==, and inequivalence as =/=. Note that these operators are associative, and even mutually associative: (P == Q) =/= R is equivalent to P == (Q =/= R).
• Implication is written as =>, and reverse implication as <=. (Yes, this is an ambiguity with the 'at most' operator, which I also write as <=. Let me know if you have a solution for this.)
• Logical 'and' and 'or' are written as /\ and \/.
• Logical negation is written as !.
• Function application ('the f of x') is written using an infix dot, as f.x.
• 'x is an element of set s' is also written as s.x: a set is seen as a function that returns a boolean true when the value is in the set, and false otherwise.

```Changes to calc/calc-not.html:

Sat Apr 30 09:32:00 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
* Updated links to Gries' book 'A Logical Approach to Discrete Math'.

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
* Move from CVS to darcs: do not show the CVS date anymore.

Thu Feb  7 19:43:35 MET 2002  marnix
* Updated all files to use the m4 template

Wed Sep  5 21:20:00 MEST 2001  marnix
* Made explicit that last changed date is in GMT

Wed Sep  5 21:08:51 MEST 2001  marnix
* Now 'last changed' is on its own line

Wed Sep  5 10:10:47 MEST 2001  marnix