- URL: https://courses.engr.illinois.edu/cs576/sp2015/doc/isar-overview.pdf
- Title: A Tutorial Introduction to Structured Isar Proofs
- Author: Tobias Nipkow
ブラケットは檜山が挿入。
a [tactic] proof is a more or less structured sequence of commands that manipulate an implicit proof state. Thus the proof text is only suitable for the machine; for a human, the proof only comes alive when he can see the state changes caused by the stepwise execution of the commands. Such proofs are like uncommented assembly language programs.
Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few experts.
arduous ： つらい
