- David Gries & Fred B Schneider
- Teaching Math More Effecively Through Calculational Proofs
- Am Math Monthly V102n8(Oct 1995)pp691-697)
- =ADVERT CALCULATIONAL LOGIC MATHEMATICS
- Advert for
[GriesSchneider93]
- 15 axioms and 4 rules
- = is transitive, can substitute a free variable,
- equanimity:
- if P and (P ≡ Q) then Q
- and Liebnitz:
- E[v:=P]
- = <P=Q>
- E[v:=Q]

Where P and Q are expressions and v some variable not found in P or Q and E[v:=P] some expression with every ovccurrence of v replaced by P and E[v:=Q] the same expression with every v replaced by Q.Also treats ≡ as an associative (serial) operator, and equals as a parallel operator.

Unified notation for all quantification, summation, etc:

- (op var | condition : expression)
Formal notation is a repository of facts and a means of clarification. It provides rules for judging the soundness of inference and detecting and eliminating ambiguity.

Search for bibliographic items containing a matching string.

Search for a specific bibliographic item by name.

To see the complete bibliography (1Mb+) select:[Bibliography]