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.

This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page.

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
  * Added date last changed

Wed Sep  5 08:50:24 MEST 2001  marnix
  * Initial revision