David Gries Position statement on Formal methods

University of Georgia

Logic is the glue that binds together
arguments in all domains

A skill at using formal methods that rely on propositional and predicate requires not only knowledge of those languages but also some skill in using them to prove things. But traditional logics were designed to help people study logics, not use them as everyday tools.

Calculational logic, in which substitution of equals for equals rather than modus ponens is the main inference rule can be used in all domains --it can be extended easily to a theory of sets, to a theory of arithmetic, to a theory of sequences, to a theory of functions and relations, to group theory, and so on. Calculational logic is a formalization of how many mathematicians carry our proofs.

And it is possible to instil in students a skill in using calculational logic. Our experience is that students are far more positive about notation, proof, and rigor with our treatment than they are after a conventional discrete math course. Many students say that they are now less apprehensive about mathematics and proof, and others say they are using their new skill in formal manipulation in other courses. Some teachers who have used our text (in primarily teaching institutions) say that the approach helps the weaker students more than the stronger ones.

Thus,we believe that learning calculational logic can change one's view of logic and formal methods, giving one an appreciation of formality and its uses as well as a skill in using it.

For more information, see the URL http://www.cs.uga.edu/~gries/Logic/Introduction.html