C* 中的后向证明

EN | 中文

前一节我们以前向方式构造证明：从证明树的叶子，也就是公理和已知定理出发，逐步应用推理规则，直到得到所需的结论。这个方向常常不符合直觉。人们更愿意从想要证明的结论出发，将它分解为更简单的子目标，直到每个子目标都能直接证明，再构造出真正的定理。这就是后向证明，也称目标导向证明。

基于 LCF 架构的证明一节已经结合 ML/HOL Light 介绍了这一思想，以及策略（tactic）、目标栈（goalstack）和验证函数（validation）这些概念。本节介绍 C* 中的具体实现。C 没有闭包，无法在闭包中隐含地表示证明树，因此 C* 将树表示为一种可以查看和操作的显式数据结构。我们先用 R. Milner 的通用目标寻求理论说明这一设计的基础，最后用 C 编写并组合策略。

前向与后向：从一个例子开始

证明系统提供一组推理规则。每条规则都说明：有了与其前提匹配的定理，就可以构造出与其结论匹配的定理。C* 的 HOL 接口提供的规则包括以下三条：

前向。前向证明按依赖顺序调用规则，生成一串定理：


[[cst::proof]] {
  // 先构造两个叶子定理，再按依赖自底向上组合
  thm p_th   = assume_rule(`P:bool`);        // P |- P
  thm q_th   = assume_rule(`Q:bool`);        // Q |- Q
  thm pq_th  = conj_rule(p_th, q_th);        // P,Q |- P && Q
  thm q_imp  = disch_rule(`Q:bool`, pq_th);  // P |- Q ==> P && Q
  thm result = disch_rule(`P:bool`, q_imp);  // |- P ==> Q ==> P && Q
}


[[cst::proof]] {
  // 先构造两个叶子定理，再按依赖自底向上组合
  thm p_th   = assume_rule(`P:bool`);        // P |- P
  thm q_th   = assume_rule(`Q:bool`);        // Q |- Q
  thm pq_th  = conj_rule(p_th, q_th);        // P,Q |- P && Q
  thm q_imp  = disch_rule(`Q:bool`, pq_th);  // P |- Q ==> P && Q
  thm result = disch_rule(`P:bool`, q_imp);  // |- P ==> Q ==> P && Q
}

调用顺序由推导的依赖关系决定：先有 p_thp_th 与 q_thq_th，才能调用 conj_ruleconj_rule；得到合取结果后，才能依次调用 disch_ruledisch_rule，最终得到 resultresult。

后向。后向证明根据结论的形态逐步分解目标，构造出一棵证明树（也称目标树）：

蓝色箭头表示自顶向下分解目标；绿色箭头表示在分解完成后自底向上遍历树，依次调用推理规则构造定理。

最外层连接词是蕴含，与 disch_ruledisch_rule 的结论匹配，因此我们将蕴含的前件移入上下文，以后件为新的待证目标。再次使用 disch_ruledisch_rule，重复这一操作。此时目标是合取，与 conj_ruleconj_rule 的结论匹配，可以拆分为两个子目标，各自由 assume_ruleassume_rule 直接解决。分解到此结束。

分解完成后，我们自底向上遍历树，在每个节点调用一条推理规则，构造达成该节点目标的定理，直到得到树根处的定理，也就是最初想要证明的定理。

Milner 的目标寻求理论

这一过程分为两个阶段，在什么条件下才可信呢？Milner 给出了一个通用的目标寻求理论（Goal-Seeking Theory）来回答这个问题，其适用范围不限于定理证明。该理论从两类对象及它们之间的关系出发。设

为目标的集合，；
为事件的集合，；
为达成关系（Achievement Relation）；意为事件达成目标。

定义 1（策略与验证函数）。对集合，记为上的有限列表，为偏函数。验证函数是从事件列表到事件的偏函数；记为全体验证函数的集合。
策略是一个偏函数，将一个目标映射到一个子目标列表和一个验证函数：
当在处有定义时，将其结果记为，其中为子目标列表。当各个事件分别达成对应的时，验证函数接收这些事件组成的列表，并重建一个候选的上层事件：。

因此，一轮完整的目标导向推理包含两个阶段：先后向分解，再前向验证。

策略的两个方向：目标产生子目标（蓝色）；子目标的达成事件重建上层事件（绿色）。

后向构造只是拟定了一份达成计划，说明为了达成必须先达成哪些目标，同时记录稍后要用的验证函数。只有在达成各个子目标的事件实际发生后，才会调用，前向构造出上层事件。

一个日常例子。我们用出行计划来具体说明这些对象。顶层目标是。策略将它拆分，并保存验证函数：

其中是“Alice 在7:30时带着行李在楼下”，是“Bob 在7:30开车到达”。另一个策略将进一步拆分：， = “Bob 7点起床”， = “车能发动”。目前只有子目标和验证函数，这些事件都还没有发生。

进入前向阶段，假设事件分别达成。验证函数按依赖顺序执行：

这里是“Bob 开车出发，不晚于7:30抵达 Alice 楼下”，是“Bob 接上 Alice 后开往机场”。如果这两次应用策略都有效，则，进而。后向阶段确定还需要达成什么以及稍后如何组合；前向阶段则从实际发生的事件出发，逐层构造出达成顶层目标的事件。

有效性

定义 2（有效策略）。设。策略在处有效，记为，当且仅当：
其中表示验证函数在该事件列表上有定义。因此，有效性不仅要求结果能达成上层目标，还要求：对于任何合法的事件列表，只要其中的事件分别达成对应的子目标，验证函数就必须能产生结果。
若此条件对定义域内的每个目标都成立，则是一个有效策略，记为。

为什么后向策略不需要额外信任

在 LCF 风格的定理证明中，这些抽象对象有了具体的含义：事件就是定理，目标就是目标相继式。它们之间的达成关系定义如下：

定义 3（定理何时达成目标）。 定理达成目标，记为，当且仅当与是等价的，且中的每条假设在中都有一条与之等价的假设。

在函数式元语言（ML、Haskell……）中，验证函数就是一个接受定理列表并返回定理的高阶函数，因此经典的策略类型写作：


type tactic     = goal -> goal list * validation
type validation = thm list -> thm


type tactic     = goal -> goal list * validation
type validation = thm list -> thm

每次应用策略，不仅返回子目标，还返回一个验证闭包。THENTHEN 和 THENLTHENL 等策略组合子同时组合策略及其验证闭包，因此整个达成计划隐含在嵌套的高阶函数之中。

这样做的好处，正是前文讨论可信内核时说明的。后向证明最终要调用验证函数，而验证函数只能通过推理规则组合已有定理。分解过程或验证函数中的错误，可能使它无法构造达成上层目标的定理，但绝不可能使它证明不成立的目标。

C* 中的显式目标树

经典策略组合子将多个验证闭包组合在一起，证明树就隐含在这些闭包的嵌套之中。C 没有原生闭包，因此 C* 将树直接表示为用户可见的数据结构，称为目标树（Goal Tree）：


typedef thm (*valid_fun)(thm_list, gnode);
typedef struct goal_node {
  goal       g;
  thm        solved;
  gnode_list children;
  valid_fun  valid;
  void      *env;
} *gnode;


typedef thm (*valid_fun)(thm_list, gnode);
typedef struct goal_node {
  goal       g;
  thm        solved;
  gnode_list children;
  valid_fun  valid;
  void      *env;
} *gnode;

这一结构与 Milner 框架的对应关系如下：

Milner 框架	*C 目标树**
目标（goal）	`goalgoal`
事件（event）	`thmthm`
子目标（subgoals）	`gnode->childrengnode->children`
验证函数	`gnode->validgnode->valid` 与 `envenv`
达成关系	`gnode_acceptgnode_accept` 中的检查
执行计划	`gnode_provegnode_prove`

目标树只提供少量原始接口：

接口	在达成计划中的角色
`gnode_new_with_ccl(ccl)gnode_new_with_ccl(ccl)`	创建一个以 `cclccl` 为结论的开放根目标
`gnode_expand(g, subgoals, valid, env)gnode_expand(g, subgoals, valid, env)`	将 `gg` 展开为一个子目标列表并安装验证函数
`gnode_leaves(root)gnode_leaves(root)`	按深度优先、从左到右的顺序返回开放目标
`gnode_accept(g, th)gnode_accept(g, th)`	直接提供一个定理并立即检查其是否达成目标
`gnode_prove(root)gnode_prove(root)`	自底向上运行已展开节点的验证函数

每个节点经历三种状态：

策略将节点展开为子节点；子节点的目标均达成后，验证函数求解已展开的节点。

开放叶节点有一个目标，但没有定理、子节点或验证函数；
已展开节点持有策略创建的子节点、验证函数和环境；
已求解节点持有一条达成该节点目标的定理。

一个展开树的策略：`DISCH_TACDISCH_TAC`

其逻辑规约是：


        Gamma, HP:p ?- q
-------------------------------- DISCH_TAC "HP"
        Gamma ?- p ==> q


        Gamma, HP:p ?- q
-------------------------------- DISCH_TAC "HP"
        Gamma ?- p ==> q

自底向上看，这条规则将蕴含式结论的前件加入假设，以后件为子目标：


static thm disch_valid(thm_list ths, gnode gn) {
  term p = ((disch_env *)gn->env)->antecedent;
  return disch_rule(p, ths[0]);
}
gnode DISCH_TAC(gnode gn, const char *label) {
  term p = dest_imp(goal_ccl(gn->g)).tm1;
  term q = dest_imp(goal_ccl(gn->g)).tm2;
  goal child = general_goal_new(append_assumption(gn, label, p), q);
  return gnode_expand(gn, LIST_GOAL(child), disch_valid,
                      make_disch_env(p))[0];
}


static thm disch_valid(thm_list ths, gnode gn) {
  term p = ((disch_env *)gn->env)->antecedent;
  return disch_rule(p, ths[0]);
}
gnode DISCH_TAC(gnode gn, const char *label) {
  term p = dest_imp(goal_ccl(gn->g)).tm1;
  term q = dest_imp(goal_ccl(gn->g)).tm2;
  goal child = general_goal_new(append_assumption(gn, label, p), q);
  return gnode_expand(gn, LIST_GOAL(child), disch_valid,
                      make_disch_env(p))[0];
}

代码依次完成四步：提取蕴含的前件和后件；将前件作为带标签的假设加入子目标；在 envenv 中保存前件，供验证函数稍后使用；最后用 gnode_expandgnode_expand 设置子节点、验证函数和环境。后向阶段只构造以后件为结论的子目标；前向阶段收到达成该子目标的定理后，调用 disch_ruledisch_rule 重建上层目标的蕴含式。

`gnode_provegnode_prove` 运行验证函数

核心递归如下：


thm gnode_prove_internal(gnode gn) {
  if (gn->solved != empty_theorem) return gn->solved;
  thm_list child_ths = THM_LIST();
  for (size_t i = 0; i < vector_size(gn->children); ++i)
    vector_add(&child_ths, gnode_prove_internal(gn->children[i]));
  thm result = gn->valid(child_ths, gn);
  gnode_accept(gn, result);
  return result;
}


thm gnode_prove_internal(gnode gn) {
  if (gn->solved != empty_theorem) return gn->solved;
  thm_list child_ths = THM_LIST();
  for (size_t i = 0; i < vector_size(gn->children); ++i)
    vector_add(&child_ths, gnode_prove_internal(gn->children[i]));
  thm result = gn->valid(child_ths, gn);
  gnode_accept(gn, result);
  return result;
}

gnode_provegnode_prove 不会搜索证明，也不会替你应用策略。它只遍历已经建好的树，从左到右收集子节点的定理，自底向上运行验证函数。如果遇到开放叶节点或缺少验证函数的节点，它必然失败。最外层调用还会在返回前将约束变量名调整为与根目标一致，使最终结论与最初写下的根目标完全相同，而不只是等价。

使用与编写策略

首先，按目标形态选择策略

当前关注点	常用策略
结论的外层结构	`GEN_TACGEN_TAC`, `EXISTS_TACEXISTS_TAC`, `DISCH_TACDISCH_TAC`, `CONJ_TACCONJ_TAC`, `EQ_TACEQ_TAC`
普通假设的结构	`ASMP_CONJ_TACASMP_CONJ_TAC`, `ASMP_DISJ_TACASMP_DISJ_TAC`, `ASMP_EXISTS_TACASMP_EXISTS_TAC`
使用已有定理	`MATCH_MP_TACMATCH_MP_TAC`, `MATCH_ACCEPT_TACMATCH_ACCEPT_TAC`, `ASSUME_TACASSUME_TAC`
分类讨论与归纳	`BOOL_CASES_TACBOOL_CASES_TAC`, `CASES_TACCASES_TAC`, `INDUCT_TACINDUCT_TAC`
求解叶节点	`CONV_TACCONV_TAC`, `CONV_WITH_ASMP_TACCONV_WITH_ASMP_TAC`, `RULE_TACRULE_TAC`
移动与匹配	`REVERT_TACREVERT_TAC`, `SPEC_TACSPEC_TAC`, `INTRO_TACINTRO_TAC`, `INTROS_TACINTROS_TAC`

粗略地说，处理蕴含目标时要引入前件，处理合取目标时要将它拆分为两部分，处理全称目标时要引入新变量，处理存在目标时则要提供一个例证。每一步的输出形态都很明确，后向推理因此有了明确的方向。

下表列出了由结论驱动的策略，以及对应验证函数所调用的规则：

策略	后向规约	验证
`GEN_TAC(g,"x")GEN_TAC(g,"x")`	`!u. P u!u. P u` → `P xP x`	`gen_rulegen_rule`
`EXISTS_TAC(g,w)EXISTS_TAC(g,w)`	`?u. P u?u. P u` → `P wP w`	`exists_ruleexists_rule`
`DISCH_TAC(g,"H")DISCH_TAC(g,"H")`	`p ==> qp ==> q` → `H:p ?- qH:p ?- q`	`disch_ruledisch_rule`
`CONJ_TAC(g)CONJ_TAC(g)`	`p && qp && q` → 两个子目标 `pp`、`qq`	`conj_ruleconj_rule`
`DISJ1_TAC(g)DISJ1_TAC(g)` / `DISJ2_TAC(g)DISJ2_TAC(g)`	`p \|\| qp \|\| q` → `pp` / → `qq`	`disj1_ruledisj1_rule` / `disj2_ruledisj2_rule`
`EQ_TAC(g)EQ_TAC(g)`	`p <=> qp <=> q` → 两个蕴含方向	`undisch_ruleundisch_rule` + `deduct_antisym_rulededuct_antisym_rule`
`MATCH_MP_TAC(g,th)MATCH_MP_TAC(g,th)`	匹配 `thth` 的后件；实例化后的前件成为子目标	`mp_rulemp_rule` + 实例化
`CONV_TAC(g,cv)CONV_TAC(g,cv)`	通过 `p = qp = q` 将目标 `pp` 重写为 `qq`	`sym_rulesym_rule` + `eq_mp_ruleeq_mp_rule`

编写策略的方法

与 DISCH_TACDISCH_TAC 类似，编写一个新的 C* 策略可以分为四步：

明确可接受的目标形态及后向变换，包括子目标的数量与固定顺序；
从上层目标中提取验证函数所需的项或定理，保存在 envenv 中；
创建子节点，用 gnode_expandgnode_expand 在上层节点中设置子节点、验证函数和 envenv；
在验证函数中，按子节点的顺序接收达成各个子目标的定理，并仅调用 HOL 推理规则来重建上层定理。

例一：第一个小目标

我们再来证明上文的定理 |- P ==> Q ==> P && Q|- P ==> Q ==> P && Q，这次用策略构造证明：


gnode root = gnode_new_with_ccl(
    `(P:bool) ==> (Q:bool) ==> P && Q`);
gnode intro_p = DISCH_TAC(root, "HP");
gnode intro_q = DISCH_TAC(intro_p, "HQ");
gnode_list leaves = CONJ_TAC(intro_q);
ACCEPT_TAC(leaves[0], assume_rule(`P:bool`));
ACCEPT_TAC(leaves[1], assume_rule(`Q:bool`));
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(
    `(P:bool) ==> (Q:bool) ==> P && Q`);
gnode intro_p = DISCH_TAC(root, "HP");
gnode intro_q = DISCH_TAC(intro_p, "HQ");
gnode_list leaves = CONJ_TAC(intro_q);
ACCEPT_TAC(leaves[0], assume_rule(`P:bool`));
ACCEPT_TAC(leaves[1], assume_rule(`Q:bool`));
thm result = gnode_prove(root);

两次 DISCH_TACDISCH_TAC 引入前件，CONJ_TACCONJ_TAC 拆分合取，ACCEPT_TACACCEPT_TAC 用定理求解各个叶节点。最后，gnode_provegnode_prove 自底向上遍历树，构造出根节点的定理。

例二：有分支的证明

证明 |- (p && (q || r)) ==> ((p && q) || (p && r))|- (p && (q || r)) ==> ((p && q) || (p && r))：


gnode root = gnode_new_with_ccl(`
  ((p:bool) && (q || r)) ==>
  ((p && q) || (p && r))
`);
gnode body = DISCH_TAC(root, "H");
body = ASMP_CONJ_TAC(body, "H", "HP", "HQR");
gnode_list branches = ASMP_DISJ_TAC(body, "HQR", "HQ", "HR");
gnode left = DISJ1_TAC(branches[0]);
gnode_list lp = CONJ_TAC(left);
ACCEPT_TAC(lp[0], assume_rule(`p:bool`));
ACCEPT_TAC(lp[1], assume_rule(`q:bool`));
gnode right = DISJ2_TAC(branches[1]);
gnode_list rp = CONJ_TAC(right);
ACCEPT_TAC(rp[0], assume_rule(`p:bool`));
ACCEPT_TAC(rp[1], assume_rule(`r:bool`));
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(`
  ((p:bool) && (q || r)) ==>
  ((p && q) || (p && r))
`);
gnode body = DISCH_TAC(root, "H");
body = ASMP_CONJ_TAC(body, "H", "HP", "HQR");
gnode_list branches = ASMP_DISJ_TAC(body, "HQR", "HQ", "HR");
gnode left = DISJ1_TAC(branches[0]);
gnode_list lp = CONJ_TAC(left);
ACCEPT_TAC(lp[0], assume_rule(`p:bool`));
ACCEPT_TAC(lp[1], assume_rule(`q:bool`));
gnode right = DISJ2_TAC(branches[1]);
gnode_list rp = CONJ_TAC(right);
ACCEPT_TAC(rp[0], assume_rule(`p:bool`));
ACCEPT_TAC(rp[1], assume_rule(`r:bool`));
thm result = gnode_prove(root);

ASMP_DISJ_TACASMP_DISJ_TAC 产生两个独立的子目标，分别对应两个析取支：


#0  HP:p, HQ:q |-? (p && q) || (p && r)
#1  HP:p, HR:r |-? (p && q) || (p && r)


#0  HP:p, HQ:q |-? (p && q) || (p && r)
#1  HP:p, HR:r |-? (p && q) || (p && r)

如果从一个新的根目标出发，可以用 INTRO_TACINTRO_TAC 的引入模式，将上述三行代码中引入并分解假设的操作合并为一步：


gnode root2 = gnode_new_with_ccl(goal_ccl(root->g));
gnode_list branches2 = INTRO_TAC(root2, "HP & (HQ | HR)");


gnode root2 = gnode_new_with_ccl(goal_ccl(root->g));
gnode_list branches2 = INTRO_TAC(root2, "HP & (HQ | HR)");

例三：苏格拉底式推理

证明 |- ((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==> mortal(Socrates)|- ((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==> mortal(Socrates)：


gnode root = gnode_new_with_ccl(`
  (((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==>
    mortal(Socrates))
`);
gnode body = INTRO_TAC(root, "Hall & Hman")[0];
thm socrates_rule =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hall"))[0]);
body = MATCH_MP_TAC(body, socrates_rule);
thm man_socrates =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hman"))[0]);
ACCEPT_TAC(body, man_socrates);
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(`
  (((!x:A. man(x) ==> mortal(x)) /\ man(Socrates)) ==>
    mortal(Socrates))
`);
gnode body = INTRO_TAC(root, "Hall & Hman")[0];
thm socrates_rule =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hall"))[0]);
body = MATCH_MP_TAC(body, socrates_rule);
thm man_socrates =
    assume_rule(gnode_get_asmps(body, CONST_STRING_LIST("Hman"))[0]);
ACCEPT_TAC(body, man_socrates);
thm result = gnode_prove(root);

我们先取出假设 Hall: !x:A. man(x) ==> mortal(x)Hall: !x:A. man(x) ==> mortal(x)。MATCH_MP_TACMATCH_MP_TAC 将其后件与当前目标 mortal(Socrates)mortal(Socrates) 匹配，把目标转换为实例化后的前件 man(Socrates)man(Socrates)。随后，ACCEPT_TACACCEPT_TAC 用 HmanHman 假设解决这个目标。

例四：从目标中恢复归纳实例

定义列表类型和 appendappend：


indtype nlist = new_datatype_definition(
    "nlist = nil"
    "      | cons num nlist");
thm app_def = new_rec_definition(
    nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);


indtype nlist = new_datatype_definition(
    "nlist = nil"
    "      | cons num nlist");
thm app_def = new_rec_definition(
    nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);

然后证明 |- !l:nlist. app l nil = l|- !l:nlist. app l nil = l。

这个右单位元性质的前向证明需要用户先证明基本情况和归纳步骤，再用 spec_rulespec_rule 和归约，手动将归纳定理实例化到谓词 \l. app l nil = l\l. app l nil = l。选择这些参数时，目标完全不参与其中。在后向证明中，这些信息可以由目标提供：


gnode root = gnode_new_with_ccl(
    `!l:nlist. app l nil = l`);
gnode_list cases =
    CONJ_TAC(MATCH_MP_TAC(root, nlist.ind));
CONV_TAC(cases[0], rewrite_conv(THM_LIST(app_def)));
gnode step = INTROS_TAC(
    cases[1], CONST_STRING_LIST("h", "t", "IH"))[0];
CONV_WITH_ASMP_TAC(step, rewrite_conv, THM_LIST(app_def));
thm result = gnode_prove(root);


gnode root = gnode_new_with_ccl(
    `!l:nlist. app l nil = l`);
gnode_list cases =
    CONJ_TAC(MATCH_MP_TAC(root, nlist.ind));
CONV_TAC(cases[0], rewrite_conv(THM_LIST(app_def)));
gnode step = INTROS_TAC(
    cases[1], CONST_STRING_LIST("h", "t", "IH"))[0];
CONV_WITH_ASMP_TAC(step, rewrite_conv, THM_LIST(app_def));
thm result = gnode_prove(root);

MATCH_MP_TACMATCH_MP_TAC 将归纳定理的后件 !l. P(l)!l. P(l) 与当前目标匹配，自动恢复出 P := \l. app l nil = lP := \l. app l nil = l。再将所得的合取拆分为两个开放目标：


#0  ?- app nil nil = nil
#1  ?- !h t. app t nil = t ==>
        app (cons h t) nil = cons h t


#0  ?- app nil nil = nil
#1  ?- !h t. app t nil = t ==>
        app (cons h t) nil = cons h t

基本情况可以通过 app_defapp_def 重写来解决；归纳步骤先引入 hh、tt、IHIH，再用 app_defapp_def 和 IHIH 重写。目标已经确定了匹配的输出形态，因此用户无需编写 spec_rulespec_rule 调用。

小结

Milner 的策略同时返回子目标和验证函数：后向阶段拟定达成计划，前向阶段运行验证函数。有效性是一条全称语义规约，要求对所有合法的子目标达成事件都成立。
策略程序不进入可信内核；最终定理仍由 HOL 推理规则构造，并由每个目标节点接受。策略中的错误可能导致证明失败，但绝不可能使它证明不成立的目标。
经典 LCF 将证明树隐含在高阶函数和闭包之中；C* 没有闭包，因此将同样的结构显式表示为 goal_nodegoal_node，提供少量原始接口（gnode_new_with_cclgnode_new_with_ccl、gnode_expandgnode_expand、gnode_leavesgnode_leaves、gnode_acceptgnode_accept、gnode_provegnode_prove），以及 DISCH_TACDISCH_TAC 等用于展开目标树的策略。
后向证明由目标驱动：目标的形态决定策略的选择，甚至可以用来恢复实例化信息，而前向证明需要手动提供这些信息。MATCH_MP_TACMATCH_MP_TAC 对归纳定理的应用就是一个例子。

C* 中的后向证明

前向与后向：从一个例子开始

Milner 的目标寻求理论

有效性

为什么后向策略不需要额外信任

C* 中的显式目标树

一个展开树的策略：DISCH_TACDISCH_TAC

gnode_provegnode_prove 运行验证函数

使用与编写策略

首先，按目标形态选择策略

编写策略的方法

例一：第一个小目标

例二：有分支的证明

例三：苏格拉底式推理

例四：从目标中恢复归纳实例

小结

一个展开树的策略：`DISCH_TACDISCH_TAC`

`gnode_provegnode_prove` 运行验证函数