agentzh さんのプロフィールHuman ＆ Machineフォトブログリストその他

ヘルプ

ブログ

概要

並べ替え:

<< 最初へ < 前へ次へ > 最後へ >>

2月6日

NAME

KB - VRG 知识库简介

AUTHOR

Agent Zhang (章亦春) <agentzh at gmail dot com>

VERSION

   Maintainer: Agent Zhang <agentzh at gmail dot com>
   Date: 26 Dec 2006
   Last Modified: 26 Dec 2006
   Version: 0.01

DESCRIPTION

这篇文档将简要地介绍一下 VRG 立体几何定性证明系统的知识库。如果您对 VRG 项目还不熟悉，请先阅读该项目的 Overview 文档。:)

记法约定

VRG 知识库使用 XClips 语言进行描述。为方便起见，在本文档中的规则和事实示例亦使用 XClips 记法。VRG 定义了如下的特有运算符：

前缀 (prefix) \ 表示谓词名 line，例如 \a 等同于 line(a).
前缀 # 表示谓词名 plane，例如 #alpha 等同于 plane(alpha).
中缀 (infix) T 等同于谓词名 orthogonal，表示正交或者垂直关系。
中缀 // 等同于谓词名 parallel，表示平行关系。
中缀 X 等同于谓词名 cross, 表示既不平行也不垂直的关系（在 VRG 内部术语中，称此种关系为 “斜交关系”）。
中前缀 (infix-prefix) ~ 表示谓词名前缀 not_, 例如 a [~//] b 等价于space_not_parallel(a, b).
中包围缀 (infix-circumfix) [ ] 表示立体几何空间中的关系，比如 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://perlcabal.org/~agentzh/slides/xclips/xclips.pdf

知识库的建模对象

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 在立几空间中的推理任务主要是将复杂的关系分解为基本关系，或者将基本关系合成为复杂关系。

基本假设条件

目前，知识库使用了下列假设条件：

若一平面与另一平面的名称不同，则认为两平面不重合。（知识库自身创建的“辅助平面”除外。）
若一直线与另一直线的名称不同，则认为两直线不重合。（知识库自身创建的“辅助直线”除外。）

取消这两条基本假设虽然从逻辑上更加完整，但从实用性的角度上讲，将不可避免地使知识库中到处充斥着“a 与 b 不重合”这样的断言，同时也会增加了用户输入已知条件的负担，增加了因人为的已知条件不充足而无法求证的可能性。

知识库的推理流程

知识库从物理上分为 4 个 CLIPS 模块(module)，亦对应推理流程的 4 大阶段：

Vectorize 模块: Vectorize 模块是由 preprocess.xclp 和 vectorize.xclp 这两个文件实现的。该模块负责完成从几何空间内的线线关系、线面关系、面面关系及其他复杂关系到向量空间内的向量关系的转换。
Eval 模块: Eval 模块是由 vector-eval.xclp 文件实现。该模块负责在向量空间内执行推理，从已知的向量关系不断推出新的向量关系。
AntiVectorize 模块: 此模块由 anti-vectorize.xclp 文件实现。它负责执行 Vectorize 模块的“逆操作”，即将新的向量关系还原为几何空间中的线线关系、线面关系和面面关系。
GoalMatch 模块: GoalMatch 模块完成用户给定的证明目标在所有已知事实中的匹配及相关的解释工作。

当推理机的焦点处于某个模块时，只有属于该模块的规则和事实才能被参与推理。

有关立几空间的事实由 Vectorize 模块，AntiVectorize，和 GoalMatch 模块共享；有关向量空间的事实由 Vectorize 模块，Eval 模块，和 AntiVectorize 模块共享。

推理机运行的具体流程如下

用户输入的已知条件所对应的“初始事实”被导入到 Vectorize 模块。
推理机焦点 (focus) 从默认模块 MAIN 切换至 Vectorize 模块，执行立几空间内的关系演算和“向量化”操作。
上一步运行完毕后，再将焦点移至 Eval 模块，执行向量空间内的关系演算，推出更多的向量关系。
将焦点移至 AntiVectorize 模块，对所有新的向量关系执行反向量化，还原出立几空间中的语义。
焦点被切换至 GoalMatch 模块，使用用户给定的证明目标对所有已知事实进行匹配，并生成解释和评价。

知识库的内部结构

知识库由下列 XClips 源文件构成：

vrg-sugar.xclp

该文件定义了知识库中所使用的特殊的运算符，例如前缀 \ 和中缀 //.该文件为知识库中所有其他 .xclp 文件所包含。详情请参与记法约定.

例如前缀 \ 的定义如下：

    prefix:<\>   line

而中缀 // 的定义如下：

    infix:<//>   parallel

preprocess.xclp

该文件定义了 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.
```

vectorize.xclp

本文件包含了执行“向量化”步骤的所有规则。

线线关系的向量化

若直线 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.

vector-eval.xclp

此文件中的规则都是向量空间内的“求解规则”，用于从已知的向量关系推出全新的向量关系。这些规则是整个 VRG 系统知识的核心。

已知 a, b, c 都是向量，若 a // b, b 与 c 满足关系 R,且 c 不同于 a，则 a 与 c 亦满足关系 R.
```
    ?a <//> ?b, ?b <?R> ?c, ?a \= ?c
    => ?a <?R> ?c.
```
这一条规则的意义是，向量间的关系可以通过“平行”关系进行传递。在立体几何空间中，许多定理、定义和推论都对应于这一条规则。
比如高中数学课本``立体几何''一章有下列公理和定理是本条向量规则在立几语义中特殊的表现形式：
- 平行公理
- 直线和平面垂直的判定定理 II
- 直线和平面垂直的性质定理
- 直线和平面垂直的性质定理 II
- 两个平面平行的性质定理 II
- 两个平面平行的性质定理 III
- 两个平面垂直的判定定理
- 直线和平面平行的判定定理
- 平行线组定理
我们看到，一条向量化规则对应到如此之多的立几定理和公理。从这个意义上讲，向量化方法有效地揭示出立体关系的本质。
已知 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.
```
这条规则揭示的是向量关系满足交换律。

anti-vectorize.xclp

本文件中的几条规则执行“逆向量化”操作，正好是 vectorize.xclp 中规则的“反函数”，比如逆向量化规则

    \?l, #?alpha, ?l <T> ?alpha => ?l [~T] ?alpha, ?l [~X] ?alpha.

的含义是：如果在向量空间中，向量 l 垂直于向量 alpha，且在立体几何空间中，l是直线，alpha 是平面，则有在立几空间中，直线 l 不垂直于平面 alpha，且直线 l 不斜交于平面 alpha.

goal-match.xclp

本文件中的规则使用用户给定的证明目标对已得到的事实进行匹配。

若用户求证 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).
```

知识库的完整性自检与 DBC

除了上述规则之外，知识库中还收录了许多自检测规则，用于检测事实库内部的完整性。这些设施可以有效地检测出用户给定事实之间的冲突、知识库规则之间的冲突，以及其他形式的 VRG bug.

事实上，在 VRG 的早期，这些自检测规则确实捕捉到不少连题库测试台都未捕捉到的 bugs。

一条典型的自检规则如下：

    \?l, #?alpha, ?l [on] ?alpha, ?l [~on] ?alpha
    => contradiction("[on]", "[~on]", ?l, ?alpha).

其含义是：一条直线要么在一个平面上，要不不在那个平面上。如果同时存在这两个事实，则生成 contradction 事实指示矛盾冲突的存在。

将完整性测试逻辑与系统自身的实现放在一起，在软件工程中称为 Design by contract (DBC).VRG 的实践表明，在基于规则的系统中实现 DBC 要比传统的命令式语言要方便和自然得多。

知识库的 Subversion 仓库

您总是可以从下面的 Subversion (SVN) 仓库取得最新版本的 VRG 知识库：

https://svn.berlios.de/svnroot/repos/unisimu/VRG/knowledge

TODO

在 line 和 plane 谓词的基础上引入 point 谓词用于显式地声明几何点。
虽然当前知识库已通过使用隐式的点对象来处理类似“两线交于一点”的条件，但显式的点对象无疑会提高规则的可读性和知识库的可扩展性。

COPYRIGHT

NAME

Overview - VRG 专家系统概览

AUTHOR

章亦春 <agentzh at gmail dot com>

计算机科学与通信工程学院江苏大学

VERSION

   Maintainer: Agent Zhang <agentzh at gmail dot com>
   Date: 24 Dec 2006
   Last Modified: 24 Dec 2006
   Version: 0.01

VRG 是什么？

VRG 是一个立体几何定性问题证明系统。比如下面这样的问题都可以使用VRG 进行证明：

若直线 l // 平面 alpha, 则 l 平行于 alpha 内的所有直线吗？
设 alpha、beta 表示平面，a、b 表示直线，则 a // alpha 的一个充分条件是不是 alpha 垂直于 beta, 且 a 垂直于 beta ?
判断平行于同一个平面的两个平面是否平行
一个平面内的两相交直线与另一个平面内的两条相交直线分别平行，则这两个平面平行吗？
若平面 alpha 垂直于平面 beta, 直线 n 在 alpha 上，直线 m 在 beta 上，m 垂直于 n, 则同时有 n 垂直于 beta 和 m 垂直于 alpha 成立吗？
PA、PO 分别是平面 alpha 的垂线、斜线，AO 是 PO 在平面 alpha 内的射影，且 a 在 alpha 上，a 垂直于 AO，则 a 垂直于 PQ.

上述问题都引用自 VRG 的自动化测试台的用例。VRG 可以对任一个用户问题作出 2 种基本判断：Yes （即可以证明）和 No（即无法确定），并且给出提示信息和证明过程。

用户如何向 VRG 描述自己的问题？

用户通过一种类似几何语言的“用户语言”向 VRG 描述自己的问题。

例如上面的第 1 题可以用 VRG 用户语言表达如下：

    line l, m;
    plane alpha;
    l // alpha, m on alpha => l // m;

第 2 题可以表达如下：

    plane alpha, beta;
    line a, b;

    alpha T beta, a T beta => a // alpha

第 3 题可以表达如下：

    plane alpha, beta, theta;
    alpha // theta, beta // theta => alpha // beta

第 4 题可以表达如下：

    line l1, l2, l3, l4;
    plane alpha, beta;
    point P, Q;

    l1 on alpha, l2 on alpha, meet(l1, l2, Q),
    l3 on beta, l4 on beta, meet(l3, l4, Q),
    l1 // l3, l2 // l4 => alpha // beta

第 5 题可以表达如下：

    plane alpha, beta;
    line m, n;

    alpha T beta, n on alpha, m on beta, m T n => n T beta, m T alpha;

第 6 题即三垂线定理，其 VRG 描述如下：

    plane alpha;
    line a;
    line b; -- line PA
    line d; -- line AO
    line c; -- line PO
    b T alpha, project(c, alpha, d), a on alpha, a T d
    =>
    a T c;

用户该如何运行 VRG 系统？

用户首先使用 VRG 用户语言描述自己的立体几何问题，并将之保存到一个磁盘文件，并使用 .vrg 作为文件扩展名。然后使用下面的命令行进行求解：

    $ perl script/vrg-run.pl foo.vrg

典型地，若将上面的第 1 题用 VRG 语言描述后保存至 problem-1.vrg文件，则运行 vrg-run 程序的情景如下：

    $ perl script/vrg-run.pl problem-1.vrg
    Yes.

    generating vectorize.png...
    generating vector-eval.png...
    generating anti-vectorize.png...
    generating problem-1.png...
    generating problem-1.vrg1.png...
    generating problem-1.vrg2.png...

输出的第一行为``Yes.''，表示成功求证。后面的输出表示 vrg-run 程序又生成了许多图片文件。其中最重要的是 problem-1.png，它以有向图的形式绘出了整个程序证明的推理过程，即系统是如何从已知事实出发一步一步推出求证目标的。而 vectorize.png 描绘的是整个证明流程中的第一大步，即“向量化”阶段的推理过程；vector-eval.png 描绘的则是第二阶段，向量空间内的推理过程；anti-vectorize.png描述的则是第三阶段，亦最后一大步，即“逆向量化”部分的推理过程。

最后生成的 2 张图片比较特别。problem-1.vrg1.png 描述的是已知条件所对应的向量关系图（即 Vector Relational Graph），而 problem-1.vrg2.png 描绘的则是推理结束后结论加已知条件所对应的向量关系图。向量关系图本身使用下面的表示约定：所有节点表示向量，黑色实线表示“垂直关系”，黑色虚线表示“既不平行，也不垂直”，红色实线表示“平行关系”，红色虚线表示“不平行关系”，而其他关系会用文字显式标出。通过“向量关系图”，用户可以看到证明过程的数学本质。

VRG 是如何绘制这些 PNG 格式的有向图的？

VRG 在内部使用 AT&T 的自由软件库 Graphviz 来生成所有的有向图。

VRG 在证明结果的描述上还有哪些特别之处？

对于多证明目标的题目，VRG 在判断不成立时，会显式地指出具体是哪些目标是未决的。而对于题目自身的条件是彼此冲突的，比如两个几何元素既平行又垂直了，VRG 也会显式地指出冲突所涉及的细节（比如哪两个元素冲突了，是哪两个关系冲突了）。

VRG 经过了怎么的测试？

我已使用高中数学教材中所有的公理、定义、定理和推论对 VRG 进行了测试（在 VRG的测试集中即对应 sanity.t 文件），此外，我还使用高三时候积累的所有相关的高考复习题对 VRG 进行了测试（在测试集中即对应 senior.t 文件）。

哪些立体几何问题是 VRG 无法求解的？

对于涉及定量关系的几何问题是无法用 VRG 进行求解的，比如角度计算问题、线段长度之类。VRG 是定性求解系统，它只能处理“垂直”、“平行”、“线在面上”这样的定性关系。

VRG 的知识库是使用什么语言描述的？

VRG 的知识库全部是使用我自主设计和实现的通用目的专家系统编程语言 XClips 进行描述的，在 VRG 源代码目录中，对应 knowledge/*.xclp 这些文件。

由于使用了可扩展的 XClips 语言，VRG 的知识库非常简洁，非常清晰。

VRG 在底层采用了什么样的推理引擎？

VRG 在底层使用了美国航空航天局约翰逊太空中心开发的正向链推理机 CLIPS. 事实上，VRG 系统与 CLIPS 的交互全部是通过 XClips 系统来完成的。XClips 正是建筑在CLIPS 之上的。

值得一提的是，CLIPS 是发布在公共域(public domain)中的，因此可以将之用于任何目的。

VRG 可以运行在哪些操作系统上？

VRG 的构件和依赖项都是高度可移植的，包括 CLIPS, perl, Graphviz, 因此可以不加修改地运行在包括 Windows, Linux, FreeBSD, Solaris 在内的多种操作系统上。目前，我只在 Windows XP 和 Windows 2000 上进行过测试。

如何获取 VRG ?

您总是可以从下面的 SVN 仓库获得 VRG 最新版本的源代码：

http://svn.berlios.de/svnroot/repos/unisimu/VRG

如何加入 VRG 的开发工作？

如果您想帮助完善 VRG 系统，请发送电子邮件告知作者。谢谢！