Deploying to gh-pages from @ d6ae935 🚀

Lean-zh · Jun 22, 2024 · cc979bc · cc979bc
1 parent fcee639
commit cc979bc
Show file tree

Hide file tree

Showing 7 changed files with 1,725 additions and 743 deletions.
diff --git a/induction_and_recursion.html b/induction_and_recursion.html
diff --git a/inductive_types.html b/inductive_types.html
diff --git a/introduction.html b/introduction.html
@@ -178,7 +178,7 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 mathematical bounds, or finding mathematical objects. A calculation can be viewed as a proof as well, and these systems,
 too, help establish mathematical claims.
 -->
-<p><strong>自动定理证明</strong>（Automated theorem proving）着眼于 &quot;寻找&quot; 证明。归结(Resolution)定理证明器、表格法(tableau)定理证明器、快速可满足性求解器(Fast satisfiability solvers)等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；还有些系统为特定的语言和问题提供搜索和决策程序，例如整数或实数上的线性或非线性表达式；像SMT（Satisfiability modulo theories）这样的架构将通用的搜索方法与特定领域的程序相结合；计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。</p>
+<p><strong>自动定理证明</strong>（Automated theorem proving）着眼于「寻找」证明。归结（Resolution）定理证明器、表格法（tableau）定理证明器、快速可满足性求解器（Fast satisfiability solvers）等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；还有些系统为特定的语言和问题提供搜索和决策程序，例如整数或实数上的线性或非线性表达式；像SMT（Satisfiability modulo theories）这样的架构将通用的搜索方法与特定领域的程序相结合；计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。</p>
 <!--
 Automated reasoning systems strive for power and efficiency, often at the expense of guaranteed soundness. Such systems
 can have bugs, and it can be difficult to ensure that the results they deliver are correct. In contrast, *interactive
@@ -189,7 +189,7 @@ <h2 id="计算机和定理证明"><a class="header" href="#计算机和定理证
 checked independently. Constructing such proofs typically requires much more input and interaction from users, but it
 allows you to obtain deeper and more complex proofs.
 -->
-<p>自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有bug，而且很难保证它们所提供的结果是正确的。相比之下，<strong>交互式定理证明器</strong>（Interactive theorem proving）侧重于 &quot;验证&quot; 证明，要求每个命题都有合适的公理基础的证明来支持。这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的 &quot;证明对象&quot;，可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，但它可以让你获得更深入、更复杂的证明。</p>
+<p>自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有bug，而且很难保证它们所提供的结果是正确的。相比之下，<strong>交互式定理证明器</strong>（Interactive theorem proving）侧重于「验证」证明，要求每个命题都有合适的公理基础的证明来支持。这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的「证明对象」，可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，但它可以让你获得更深入、更复杂的证明。</p>
 <!--
 The *Lean Theorem Prover* aims to bridge the gap between interactive and automated theorem proving, by situating
 automated tools and methods in a framework that supports user interaction and the construction of fully specified