Interpreting Naproche : an algorithmic approach to the derivation-indicator view

Abstract

In [1], Jody Azzouni proposes a derivation indicator view of mathematical practice and in particular of proofs.<br />The Naproche Project [5] takes proofs as linguistic entities whose semantics is given by corresponding formal derivations. This view is computationally implemented in the Naproche System where simple natural proof texts are automatically transformed into derivations, using techniques from computational linguistics, formal logic and automatic theorem proving. The development of the system has identified many ways in which parts of proof texts indicate elements of formal derivations. The Naproche Project can thus be seen as a support of the derivation indicator view, and we comment on some of the critique against derivation indication from this standpoint and our experience. Doing so, we extend earlier work by the second author on the relation between natural and formal proofs; since then, further development has shown the relation of DI to Naproche to be an interesting field that can (and should) be elaborated in detail.