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
}

调用顺序由推导的依赖关系决定：conj_ruleconj_rule 必须等待 p_thp_th 与 q_thq_th；每次 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 开车到 Alice 楼下，7:30 抵达”，是“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 同时组合策略及其验证闭包，因此整个达成计划隐式地嵌套在高阶函数之中。

其回报正是前一章关于可信内核的论点。因为后向证明最终要调用其验证函数，而验证函数只能将已有定理通过推理规则加以组合，一个有 bug 的分解或验证可能构造不出上层目标的定理——但它绝不可能证明一个不成立的目标。

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 推理规则构造，并在每个目标节点上被接受——因此有 bug 的策略只能失败，但绝不可能证明假目标。
经典 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` 运行验证函数