Calculational logic

Articles on calculational logic and teaching logic as a tool

Vita

Information Processing Letters (IPL) 53, 3 (10 February 1995). This special issue on the calculational method contains eight articles that discuss calculational logic or use it heavily in different areas. Besides an editorial by guest editor Roland Backhouse, there are papers by Karger and Hoare, the Mathematics of Program Construction Group in Eindhoven, the Eindhoven Tuesday Afternoon Club, Dijkstra, Gries and Schneider, Kornerup, Leino, and Back and von Wright.

Gries and Schneider. calculational propositional logic. IPL 53, 3 (February 1995), 145-152. This paper proves the soundness and completeness of calculational propositional logic by relating it to Church's logic P1.

David Gries and Fred B. Schneider. Teaching math more effectively through the design of calculational proofs. Tech. Rpt. 94-1415, March 1994. Accepted for publication in the Mathematical Monthly.

David Gries and Fred B. Schneider. A new approach to teaching mathematics. PRIMUS V, 2 (June 1995), 114-115.

David Gries. Teaching calculation and discrimination: a more effective curriculum. Comm. ACM 34, 3 (March 1991), 44-55.

David Gries. On presenting monotonicity and on EA=>AE (pdf file). This tech report describes how to deal with monotonicity in strengthening or weakening steps of a calculation, thus clarifying a currently confusing issue. The approach used here will be incorporated into the next edition of A Logical Approach. This note also give a nice proof of interchange of quantifications, (Ex | R: (A y | S: P)) => (Ay | S: (E x | R: P)), using the idea of a witness.

David Gries and Fred B. Schneider. Adding the Everywhere Operator to Propositional Logic (pdf file). A sound and complete modal propositional logic is presented in which "everywhere P has the interpretation ``P is true in all states''. The logic illustrates that the two following approaches to axiomatizing a logic need not be equivalent: (i) give axiom schemes that denote an infinite number of axioms and (ii) write a finite number of axioms in terms of propositional variables and introduce a substitution inference rule.

David Gries. Formal versus semiformal proof in teaching predicate logic: a reaction to Grantham's "Greek knuckleballs and lucky charms".pdf file . Grantham proposes to teach predicate logic with "semiformal" proofs. For the proofs of the theorems he uses as examples (which are more involved than the usual ones one sees in courses), we argue that formality and rigor makes the development of and the presentation of the proofs shorter, clearer, and easier.

David Gries. A calculational proof of Andrews's challenge.(pdf file). (html). Andrews's challenge is one of the more difficult predicate-logic theorems that is used as a benchmark for mechanical theorem provers. We offer a fairly simple proof of it in the calculational style.