- 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
- 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.