KB - VRG 解题系统的知识库简介
Maintainer: Zhang "agentzh" Yichun <agentzh@gmail.com> Date: 26 Dec 2006 Last Modified: 30 Dec 2011 Version: 0.02
这篇文档将简要地介绍一下 VRG 立体几何定性证明系统的知识库。
VRG 知识库使用 XClips 语言进行描述。为方便起见，在本文档中的规则和事实示例亦 使用 XClips 记法。VRG 定义了如下的特有运算符：
\ 表示谓词名 line，例如 \a 等同于 line(a).# 表示谓词名 plane，例如 #alpha 等同于 plane(alpha).T 等同于谓词名 orthogonal，表示正交或者垂直关系。// 等同于谓词名 parallel，表示平行关系。X 等同于谓词名 cross, 表示既不平行也不垂直的关系（在 VRG 内部术语中，称 此种关系为 “斜交关系”）。~ 表示谓词名前缀 not_, 例如 a [~//] b 等价于 space_not_parallel(a, b).[ ] 表示立体几何空间中的关系，比如 a [//] b 就等同于谓词 space_parallel(a, b)，而 a [T] b 就等同于谓词 space_orthogonal(a, b).< > 表示向量空间中的关系，例如 a <//> b 等价于谓词 vector_parallel(a, b), 而 a <~T> b 则等价于谓词 vector_not_orthogonal(a, b).特别地，以问号 (?) 起始的标识符为 XClips 变量，如 ?alpha, ?m 之类；否则为常量，如 beta 和 l.
变量一般用于规则，而常量一般出现在事实中。
这些其实都是 XClips 语言的语法。有关 XClips 语言的更多信息，请参见我的"Introduction to XClips" 讲座的幻灯片：
http://agentzh.org/misc/slides/xclips/
请在浏览器中打开播放，同时使用方向键翻页。
VRG 知识库大体上可以分为三个部分，一是在立体几何空间中的推理，二是向量空间中 的推理，三是在这两个空间之间的关系映射。
在立体几何空间中，基本的研究对象是空间直线和平面这两种立体几何元素以及它们之间的关系。 这些关系包括
对于线线关，VRG 仅处理线线关系中的平行关系，垂直关系，斜交关系，以及它们的衍生关系，例如 不平行，不垂直，不斜交等等。
VRG 仅处理线面关系中的线面平行，线面垂直，线面斜交，线在面上，以及它们的衍生关系，例如 线面不垂直，线不在面上等等。
比如：
/* line a is parallel to line b */
\a, \b, a [//] b.
/* line c is perpendicular to line d */
\c, \d, a [T] b.
/* line e is not parallel to line f */
\e, \f, e [~//] f.
VRG 仅处理面面关系中的面面平行，面面垂直，面面斜交，以及它们的衍生关系，例如面面不平行等等。
比如：
/* line l is parallel to plane alpha */
\l, #alpha, l [//] alpha.
/* line a is perpendicular to plane beta */
\a, #beta, a [T] beta.
比如下面这条事实
\a, \b, meet(a, b, A).
便指示了直线 a 和直线 b 相交于点 A.
该关系是指，一条直线在一个平面上的投影是另一条直线（或点）
下面这条 XClips 事实
\a, #A, \b, project(a, A, b).
就指明了直线 a 在平面 A 上的投影是 b.
比如下面这条事实
\a, #alpha, meet(a, alpha, P).
指示直线 a 与平面 alpha 相交点 P.
VRG 在立几空间中的推理任务主要是将复杂的关系分解为基本关系，或者将基本关系合成为复杂关系。
向量是立体几何元素的抽象表示。从数学语义上讲，立几空间中的平面在向量空间中对应其“法向量”， 而立几空间中的直线在向量空间中对应其“方向向量”。
向量空间中的关系演绎是整个证明系统的核心。VRG 正是通过从已有的向量关系推出新的向量关系，来 间接地从已有的几何关系推出新的几何关系的。
在向量空间中仅讨论下列关系：
例如
a <//> b
表示向量 a 与向量 b 平行。
例如
a <T> b
表示向量 a 与向量 b 垂直。
例如
例如
a <X> b
表示向量 a 与向量 b 斜交。
目前，知识库使用了下列假设条件：
取消这两条基本假设虽然从逻辑上更加完整，但从实用性的角度上讲，将不可避免地使知识库中 到处充斥着“a 与 b 不重合”这样的断言，同时也会增加了用户输入已知条件的负担，增加了因 人为的已知条件不充足而无法求证的可能性。
知识库从物理上分为 4 个 CLIPS 模块(module)，亦对应推理流程的 4 大阶段：
Vectorize 模块是由 preprocess.xclp 和 vectorize.xclp 这两个文件实现的。 该模块负责完成从几何空间内的线线关系、线面关系、面面关系及其他复杂关系到 向量空间内的向量关系的转换。
Eval 模块是由 vector-eval.xclp 文件实现。该模块负责在向量空间内执行推理， 从已知的向量关系不断推出新的向量关系。
此模块由 anti-vectorize.xclp 文件实现。它负责执行 Vectorize 模块的“逆操作”， 即将新的向量关系还原为几何空间中的线线关系、线面关系和面面关系。
GoalMatch 模块完成用户给定的证明目标在所有已知事实中的匹配及相关的解释工作。
当推理机的焦点处于某个模块时，只有属于该模块的规则和事实才能被参与推理。
有关立几空间的事实由 Vectorize 模块，AntiVectorize，和 GoalMatch 模块共享； 有关向量空间的事实由 Vectorize 模块，Eval 模块，和 AntiVectorize 模块共享。
推理机运行的具体流程如下
知识库由下列 XClips 源文件构成：
该文件定义了知识库中所使用的特殊的运算符，例如前缀 \ 和中缀 //. 该文件为知识库中所有其他 .xclp 文件所包含。详情请参与 "记法约定".
例如前缀 \ 的定义如下：
prefix:<\> line
而中缀 // 的定义如下：
infix:<//> parallel
该文件定义了 VRG 的“预处理规则”。这些规则的主要工作是在立几空间内部 进行关系演算，其目的在于将 project（投影）和 meet（相交）这样的复杂 关系转换为平行、垂直之类的简单关系，同时为某些基本关系生成“同构异形体”， 以简化后续的匹配工作。
具体说来，此文件包含下列几条规则：
alpha 和 beta 相交于直线 l 时，则 alpha 与 beta 不平行，并且 l 同时在 alpha 和 beta 上.
#?alpha, #?beta, meet(?alpha, ?beta, ?l)
=> ?alpha [~//] ?beta, ?l [on] ?alpha, ?l [on] ?beta.
这儿的前缀问号(?)表示为变量，而非常量。
l 和 m 相交于一点时，则存在一个平面 alpha 使得 l 和 m 都在 alpha 上，且 l 不平行于 m.
\?l, \?m, meet(?l, ?m, ?)
=>
?alpha := gensym(), #?alpha, temp(?alpha),
?l [on] ?alpha, ?m [on] ?alpha,
?l [~//] ?m.
这里的单个问号变量 (?) 表示“通配符”(wildcard).
l 和平面 alpha 相交于一点，则 l 既不平行于 alpha，也不在 alpha 之上：
\?l, #?alpha, meet(?l, ?alpha, ?) => ?l [~//] ?alpha, ?l [~on] ?alpha.
l 在平面 alpha 上的投影为直线 m，则存在一个平面 theta 使得 (1) l 与 alpha 斜交，(2) l 在 theta 上, (3) theta 与 alpha 相交于 m, 并且 (4) theta 与 alpha 垂直：
\?l, #?alpha, \?m, project(?l, ?alpha, ?m)
=>
?theta := gensym(), #?theta, temp(?theta),
?l [X] ?alpha, ?l [on] ?theta,
meet(?theta, ?alpha, ?m),
?theta [T] ?alpha.
alpha 与直线 l 之间存在某个特定的关系 R, 则 l 与 alpha 亦满足（交换律）：
#?alpha, \?l, ?alpha [?R] ?l => ?l [?R] ?alpha.
本文件包含了执行“向量化”步骤的所有规则。
若直线 l 与直线 m 之间存在关系 R, 则向量 l 与向量 m 之间 亦存在关系 R.
\?l, \?m, ?l [?R] ?m => ?l <?R> ?m.
l 与平面 alpha 垂直，则向量 l 与向量 alpha 平行：
\?l, #?alpha, ?l [T] ?alpha => ?l <//> ?alpha.
l 与平面 alpha 平行，则向量 l 与向量 alpha 垂直：
\?l, #?alpha, ?l [//] ?alpha => ?l <T> ?alpha.
l 与平面 alpha 斜交，则向量 l 与向量 alpha 亦斜交：
\?l, #?alpha, ?l [X] ?alpha => ?l <X> ?alpha.
l 在平面 alpha 上，则向量 l 与向量 alpha 垂直：
\?l, #?alpha, ?l [on] ?alpha => ?l <T> ?alpha.
\?l, #?alpha, ?l [~T] ?alpha => ?l <~//> ?alpha.
\?l, #?alpha, ?l [~//] ?alpha => ?l <~T> ?alpha.
\?l, #?alpha, ?l [~X] ?alpha => ?l <~X> ?alpha.
若平面 alpha 与平面 beta 满足关系 R, 则在向量空间中，alpha 与 beta 亦 满足关系 R.
#?alpha, #?beta, ?alpha [?R] ?beta => ?alpha <?R> ?beta.
此文件中的规则都是向量空间内的“求解规则”，用于从已知的向量关系推出全新的向量关系。 这些规则是整个 VRG 系统知识的核心。
a, b, c 都是向量，若 a // b, b 与 c 满足关系 R, 且 c 不同于 a，则 a 与 c 亦满足关系 R.
?a <//> ?b, ?b <?R> ?c, ?a \= ?c
=> ?a <?R> ?c.
这一条规则的意义是，向量间的关系可以通过“平行”关系进行传递。在立体几何空间中， 许多定理、定义和推论都对应于这一条规则。
比如高中数学课本"立体几何"一章有下列公理和定理是本条向量规则在立几语义中 特殊的表现形式：
我们看到，一条向量化规则对应到如此之多的立几定理和公理。从这个意义上讲，向 量化方法有效地揭示出立体关系的本质。
a 和 b 都是向量，若 a 垂直于向量 b, 或者 a 与 b 斜交， 则 a 不平行于 b.
?a <T> ?b; ?a <X> ?b => ?a <~//> ?b.
本规则其实揭示的其实就是“不平行”的定义。之所以专门编写一条规则来产生“不平行” 关系，是因为“不平行”在下面这条规则中扮演着关键性的角色。
a, b, c, d 四个向量满足下列关系：a 垂直于 b, b 垂直于 c, c 垂直于 d, d 垂直于 a, a 不平行于 c, 且 b 不同于 d, 则有 b // d.
?a <T> ?b, ?b <T> ?c, ?c <T> ?d, ?d <T> ?a, ?a <~//> ?c, ?b \= ?d
=> ?b <//> ?d.
在高中数学课本中有如下定理是该向量规则的“特殊表现形式”：
a 与向量 b 满足关系 R，则 b 与 a 亦满足关系 R.
?a <?R> ?b => ?b <?R> ?a.
这条规则揭示的是向量关系满足交换律。
本文件中的几条规则执行“逆向量化”操作，正好是 vectorize.xclp 中规则的“反函数”，比如 逆向量化规则
\?l, #?alpha, ?l <T> ?alpha => ?l [~T] ?alpha, ?l [~X] ?alpha.
的含义是：如果在向量空间中，向量 l 垂直于向量 alpha，且在立体几何空间中，l 是直线，alpha 是平面，则有在立几空间中，直线 l 不垂直于平面 alpha，且 直线 l 不斜交于平面 alpha.
本文件中的规则使用用户给定的证明目标对已得到的事实进行匹配。
a 与 b 在立几空间存在关系 R, 且事实库中确实存在该事实， 则生成 solved 事实指示目标已解决。
?a *[?R] ?b, ?a [?R] ?b
=> solved(space-relation, ?R, ?a, ?b).
a 与 b 在立几空间存在关系 R，且事实库中不存在该事实， 则生成 pending 事实以指示该目标“未决”。
?a *[?R] ?b, ~exists(?a [?R] ?b)
=> pending(space-relation, ?R, ?a, ?b).
a 和 b 的一求证目标未决，且事实库中存在 a 与 b 之间确定的某种关系，则生成 hint 事实，以提示用户。
pending(space-relation, ?, ?a, ?b), ?a [?R] ?b
=> hint(space-relation, ?R, ?a, ?b).
除了上述规则之外，知识库中还收录了许多自检测规则，用于检测事实库内部的完整性。 这些设施可以有效地检测出用户给定事实之间的冲突、知识库规则之间的冲突，以及其 他形式的 VRG bug.
事实上，在 VRG 的早期，这些自检测规则确实捕捉到不少连题库测试台都未捕捉到的 bugs。
一条典型的自检规则如下：
\?l, #?alpha, ?l [on] ?alpha, ?l [~on] ?alpha
=> contradiction("[on]", "[~on]", ?l, ?alpha).
其含义是：一条直线要么在一个平面上，要不不在那个平面上。如果同时存在这两个事实， 则生成 contradction 事实指示矛盾冲突的存在。
将完整性测试逻辑与系统自身的实现放在一起，在软件工程中称为 Design by contract (DBC). VRG 的实践表明，在基于规则的系统中实现 DBC 要比传统的命令式语言要方便和自然得多。
您总是可以从下面的 Git 仓库取得最新版本的 VRG 知识库：
https://github.com/agentzh/VRG-solver
line 和 plane 谓词的基础上引入 point 谓词用于显式地声明几何点。
虽然当前知识库已通过使用隐式的点对象来处理类似“两线交于一点”的条件， 但显式的点对象无疑会提高规则的可读性和知识库的可扩展性。
Zhang "agentzh" Yichun (章亦春) <agentzh@gmail.com>
Copyright 2006-2011 by Zhang "agentzh" Yichun (章亦春). All rights reserved.
VRG 解题系统概览: http://agentzh.org/misc/vrg/Overview.html