- Title: A Browsable Format for Proof Presentation
- Date: June 1996
- Authors: Jim Grundy, Turku Centre
- Pages: 8p
- URL: https://www.researchgate.net/publication/2359706_A_Browsable_Format_for_Proof_Presentation
structured calculational proof に関するフォーマットの提案。論理としては別になんてことないが、半形式証明スクリプトの構文としては参考になる。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\calc}{\Keyword{calc } }
\newcommand{\endcalc}{\Keyword{end } }
\newcommand{\theorem}{\Keyword{theorem } }
`$
- Mizar / Andrzej Trybulec (1973～現役)
- Isabelle / Lawrence Paulson (1986～現役)
- Coq / Thierry Coquand, Gérard Huet (1989～現役)
サンプル：
$`\theorem \text{sample } (k : \mrm{Nat}) : \mrm{even} ( k^3 + k) :=\\
\calc \\
\mrm{even} ( k^3 + k)\\
\updownarrow //\text{ Extract the common factor.}\\
\mrm{even} (k\cdot (k^2 + 1) ) \\
\updownarrow //\text{ Distribute even over }\cdot \text{ .}\\
\mrm{even}(k) \lor \mrm{even}(k^2 + 1) \\
\updownarrow //\text{ Simplify the right disjunct.}\\
\quad \calc \\
\quad \lnot \mrm{even}(k^2 + 1)\\
\quad \updownarrow //\text{ Since }\mrm{even}(i + 1) \text{ is }\lnot \mrm{even}(i)\\
\quad \lnot \mrm{even}(k^2 )\\
\quad \updownarrow //\text{ The defiition of square}\\
\quad \lnot \mrm{even}(k \cdot k )\\
\quad \updownarrow //\text{ Distribute }\mrm{even} \text{ over }\cdot \text{ .}\\
\quad \lnot (\mrm{even}(k)\lor \mrm{even}(k))\\
\quad \updownarrow //\text{ Disjunction is idempotent.}\\
\quad \lnot \mrm{even}(k)\\
\quad \endcalc\\
\mrm{even}(k) \lor \lnot\mrm{even}(k)\\
\updownarrow //\text{ The law of the excluded middle.}\\
\top\\
\endcalc`$
