Pyke 学习笔记（二）

规则

Pyke 通过回溯的方式，尝试每个可能的匹配。因此，同一规则可能多次适用成功，每次成功匹配的是不同的事实。在规则的 if 子句的“前提列表”中，是进还是退、是上还是下，取决于前提的证明是成功还是失败。在列表中往后退，尝试别的证明办法，这个过程叫做回溯。

推理

规则保存在规则库中，各有不同的具体内容。规则之间没有嵌套和显性关联。Pyke 必须自己设法来解决规则之间的整合，以完成某些大型任务。 Pyke 用的办法叫做“推理”，它有两种不同的方式：

1）应用正向推理规则，要求规则库已经激活。 正向推理规则可以断言新的事实，可以激活更多的规则库。 

2）当你的程序要求 Pyke 证明某个具体目标时，使用反向推理规则（例如，向 Pyke 询问）。 应用这些规则，是为了回答某个问题，而非断言新事实，或者激活更多的规则库。 反向推理规则，还能汇集 Python 函数，形成具体的“调用顺序图”或叫做“方案图”的程序，以处理实际问题。

正向推理（用 foreach 和 asssert 代替 if 和 then）

规则库激活后，正向规则执行的顺序，以其在.krb规则库文件中的次序为准。

为了进行正向推理，Pyke 查看哪个规则的 if 子句，与已知事实相匹配（ if 子句可以多次匹配成功，参见“回溯”）。 规则匹配成功后，开始启用它，将其 than 子句中的事实，加入已知事实的列表。 新的事实与其他正向规则 if 子句匹配后，可以将其启用。各种深度的推理过程，都可发生这种匹配。正向推理的过程，持续到没有规则可供使用。

规则的 if 子句中有事实陈述的模式，它们可能与几个事实匹配，于是，规则可能多次匹配启用。 规则 then 子句的事实陈述也有模式。每当规则启用，then 子句中的模式变量，可以约束成不同值，从而断言出不同事实。

注意，foreach 子句末尾的事实，可以多次匹配成功，由此多次启用 assert 子句。 

可是， foreach 子句起始的事实，仅能匹配失败一次。若匹配失败，整个规则适用失败。

例子

反向推理 （用 use 和 when 代替 then 和 if）

Pyke 的证明活动，开始于寻找某一规则，其 then 子句与目标匹配。 

Pyke 接着证明规则 if 子句为真。 

亦即：规则的 if 子句，与另一规则的 then 子句，可以建立连接。

Pyke 最终会形成一条“证据链”，从第一条规则的 if 子句开始，到下一规则的 then 子句结束。

Pyke 只允许在 use 子句里出现一个事实陈述，这与正向推理的 assert 子句（允许多个事实）不同。

在向 Pyke 求证某个目标的要求之后，这些规则才被调用。 

提出求证要求的最简方式，是用函数 some_engine.prove_1_goal 或者 some_engine.prove_goal。函数 prove_1_goal 返回找到的第一个证据后，便停止运行（或者引起意外：pyke.knowledge_engine.CanNotProve）。函数 prove_goal 返回的是求证过程中产生的全部证据的“管理器”。