![哪些软件包/实践与编写结构化推导相关?(类似于 Dijkstra 的计算证明风格)](https://linux22.com/image/247615/%E5%93%AA%E4%BA%9B%E8%BD%AF%E4%BB%B6%E5%8C%85%2F%E5%AE%9E%E8%B7%B5%E4%B8%8E%E7%BC%96%E5%86%99%E7%BB%93%E6%9E%84%E5%8C%96%E6%8E%A8%E5%AF%BC%E7%9B%B8%E5%85%B3%EF%BC%9F%EF%BC%88%E7%B1%BB%E4%BC%BC%E4%BA%8E%20Dijkstra%20%E7%9A%84%E8%AE%A1%E7%AE%97%E8%AF%81%E6%98%8E%E9%A3%8E%E6%A0%BC%EF%BC%89.png)
有谁知道有什么软件包可以支持这种风格的证明书写?
我唯一发现的是:tex-ewd,一组在 CTAN 上专门为 Dijkstra 编写的纯 TeX 宏;以及LyX 仅适用于 Windows 的版本已扩展支持结构化派生。(遗憾的是 LyX-SD 仅限于 Windows,因为我猜用 LyX 编写证明会很棒)
如果没有任何现成的包并且我必须自己动手,那么是否有足够相似的包以便我可以学习“正确的方法”来制作 LaTeX 的结构化派生包?
我首先向您表示“感谢”:) 对于任何帮助我都会非常感激。
如果您需要更多信息来提供帮助(或者即使我只是引起了您的兴趣),这里有一些很好的资源:
- 这维基百科页面
- 某种主页用于相关项目。
- 包含大量示例的 Powerpoint 演示文稿。还有颜色!http://www.risc.jku.at/conferences/cadgme2009/Back/TeachingMathLinzShort.pdf
- 包含详细信息和正式语法的论文。我附在这个问题上的示例是这篇论文的截图。http://www.tara.tcd.ie/bitstream/2262/41529/1/PEER_stage2_10.1007%252Fs00165-009-0136-5.pdf
答案1
我很想使用一系列itemize
和enumerate
环境,使用enumitem
包来帮助格式化
在下面的代码中,我使用了包resume
提供的功能enumitem
来帮助保持环境的编号,enumerate
而无需对任何数字进行硬编码。
我还使用了该命令的可选参数\item
,例如可以使用
\item[$\Vdash$]
如果你打算经常使用它,你可以把它变成\newcommand
\documentclass{article}
\usepackage{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{enumitem}
% global settings for enumerate environment
\setlist[enumerate]{label*=(\arabic*),leftmargin=0mm}
% itemize environment, when at nested depths 2, 3, 4
\setlist[itemize,2]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,3]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,4]{label=\textbullet,leftmargin=1cm}
\begin{document}
\begin{itemize}
\item Show that $f$ is continuous at $x_0$, when
\begin{enumerate}
\item\label{item:range} $f(x)=\sqrt{x}$ when $x\geq 0$, and
\item\label{item:pos} $x_0>0$
\end{enumerate}
\item[$\Vdash$] $f$ is continuous at $x_0$
\item[$\equiv$] $\{\text{definition of continuity}\}$
$(\forall\epsilon>0\cdot \exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$
\item[$\equiv$] $\{\text{choose arbitrary }\epsilon \text{generilization rule}\}$
\begin{itemize}
\item Show that $(\exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow |f(x)-f(x_0)|<\epsilon)$, when
\begin{enumerate}[resume]
\item $\epsilon>0$
\end{enumerate}
\item[$\Vdash$] $\{\text{find a suitable value for } \delta\text{ witness rule}\}$
\begin{itemize}
\item Show that $\delta>0\wedge(\forall x\geq 0\cdot|x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$, when
\begin{enumerate}[resume]
\item $\delta=?$ $\sharp$ $\delta=\epsilon\cdot\sqrt{x_0}$
\end{enumerate}
\item[$\Vdash$] $\{\text{show the two conjuncts separately, use generalization rule for second conjunct}\}$
\begin{itemize}
\item Show that $|f(x)-f(x_0)|<\epsilon$, when
\begin{enumerate}[resume]
\item\label{item:xnonneg} $x\geq 0$, and
\item $|x-x_0|<\delta$
\end{enumerate}
\item[$\Vdash$] $|f(x)-f(x_0)|$
\item[$=$] $\{$assumption \ref{item:range}, $f(x)$ and $f(x_0)$ are defined by assumptions \ref{item:xnonneg} and \ref{item:range}$\}$
\item[] $|\sqrt{x}-\sqrt{x_0}|$
\item[$=$] $\{$extend with conjugate value for $\sqrt{x}-\sqrt{x_0}$, i.e., with $\sqrt{x}+\sqrt{x_0}>0$$\}$
\item[] $\dfrac{|x-x_0|}{\sqrt{x}+\sqrt{x_0}}$
\item[$\leq$] $\{$make divisor smaller, $\sqrt{x}\geq 0$ $\}$
\end{itemize}
\end{itemize}
\end{itemize}
\end{itemize}
\end{document}
答案2
您可能对 Leslie Lamport 编写的软件包感兴趣,pf2
,用于产生结构化证明看起来与 Dijkstra 使用的风格非常相似。该包只是一个.sty
文件,似乎没有托管在 CTAN 上,但您可以在这里找到它:http://lamport.azurewebsites.net/latex/latex.html。
itemize
此包提供的样式将类似于下面这两列之一(您可以自由更改编号和缩进的样式)。我认为经过一些调整后,您可能能够实现所需的美感。好吧,可以说比使用一堆嵌套的和更轻松enumerate
。
编辑:经过一番谷歌搜索,我没有找到一种轻松创建嵌套列表的优雅方法。Markdown + KaTeX(或 MathJax)和 LaTeX 转换pandoc
可能接近这一点,但您只能获得 Markdown 环境中支持的一组有限的 LaTeX 命令。
答案3
Fokkinga 于 2015 年 1 月发布了这样一个包,它被称为计算。
它以某种方式遵循了 eqnarray 的方法(文档中如此说)。因此分数和大运算符会变得拥挤。除此之外,它还不错。