 This conviction was necessary for the birth of their innovative computer program Hyperproof, which adopts both first-order languages and diagrams (in a multi-modal system) to teach elementary logic courses (Barwise &amp; Etchemendy  1993  and Barwise &amp; Etchemendy  1994).