编辑“︁Lean自定义决策过程”︁（章节）

== 基础概念 ==
=== 决策过程的组成 ===
一个典型的自定义决策过程包含以下组件：
1. '''输入分析'''：解析当前目标或假设，提取关键信息。
2. '''推理引擎'''：应用领域特定的规则或算法进行推导。
3. '''结果生成'''：输出证明项或失败信息。

<mermaid>
graph LR
    A[输入目标] --> B{分析语法/类型}
    B -->|匹配规则| C[应用推理]
    B -->|不匹配| D[返回失败]
    C --> E[生成证明项]
    E --> F[验证并输出]
</mermaid>

=== 与内置策略的关系 ===
Lean内置了如`ring`、`linarith`等决策过程，而自定义决策过程可以通过以下方式与它们交互：
* 完全替换内置策略
* 作为预处理步骤增强内置策略
* 组合多个策略形成新策略