Elenca per:
Data
Categoria
28 febbraio
Makefile::DOM
第一阶段的工作将集中在 Makefile::DOM 的开发上。
该模块以及其他模块都将遵循“早发布，常发布”的原则，并使用先进的基于 Subversion 的 SVK 版本控制系统 进行源代码的管理。
Makefile::DOM 在 CPAN 发布的版本号，采用三段数的格式，比如 0.2.12。以此版本号为基础，可将该模块的开发工作分为下列里程碑：
0.0.x
从 0.0.1 开始，实现 MDOM::Document::Gmake 模块。它将逐步地支持 GNU make 几乎全部的词法和语法结构，完成相应的 POD 格式的英文文档，以及比较全面的基于 Test::Base 模块的 单元测试台 。
0.1.x
从 0.1.0 开始，逐步地在 MDOM （即 Makefile::DOM） 的基础上开发出 GNU make 的纯 Perl 实现（名叫 pgmake），从而得以运行 GNU make 官方的测试集 ，同时完善 MDOM::Document::Gmake ，进而确保并验证 MDOM 自身的完整性。
考虑到 GNU make 官方测试集并不是很完整，因此还须根据 GNU make Manual 文档对该测试集进行扩充，以便尽可能多地覆盖 gmake 实际支持的特性集。
0.2.x
从 0.2.0 开始，逐步实现 MDOM::Document::Nmake 模块，使得它能支持微软 32 位 NMAKE 几乎全部的词法和语法结构，完成相应的 POD 格式的英文文档，以及比较全面的基于 Test::Base 模块的单元测试台。
0.3.x
从 0.3.0 开始，在 MDOM 基础上开发出 NMAKE 的纯 Perl 实现（名叫 pnmake），从而得以运行 NMAKE 测试集，同时完成 MDOM::Document::Nmake，进而确保并验证 MDOM 自身的完整性。
由于微软的 NMAKE 不像 GNU make 那样是开源项目，我无法取得 NMAKE 官方的测试集，故必须按照 MSDN 网站上的 NMAKE Reference 文档自主设计测试用例。
0.4.x
将 GNU make 和 MS NMAKE 对应的基于 IPC::Run3 的测试集转换为针对 MDOM 的高度可移植的轻量级测试集。
0.5.x 及其以后版本
不断完善文档，不断修复自己发现的和其他用户报告的 bug，不断根据用户需求完善接口和实现。
Makefile::DOM 的 SVN 仓库位于下面的位置：
http://svn.openfoundry.org/mdom/
其结构分为 trunk （主干）和若干个 branches （分支）。主干是主流的版本；CPAN 发布总是从主干产生。而各个分支主要用于试验和演化新特性，待成熟后才``融合''回主干中去。融合工作可以由 SVK 自动完成（利用 SVK 的 smerge 命令）。反过来，主干中的更新，借助于 SVK，也可以轻易地融合到各个分支中去。
本模块计划拥有以下分支：
/branches/gmake
用于开发 Perl 版本的 GNU make 实现，pgmake，并将包含基于 IPC::Run3 和 Test::Base 的 GNU make 测试集。
pgmake 和使用了 IPC::Run3 的测试集将永不融入 /trunk ，但将成为新一代 Makefile::Parser 的 Gmake 部分的原型（prototype）。
该分支从 Makefile::DOM 0.1.x 起启用。
/branches/nmake
用于开发 Perl 版本的 NMAKE 实现，pnmake，并将包含基于 IPC::Run3 和 Test::Base 的 NMAKE 测试集。测试台框架将复用 /branches/gmake 中的 GNU make 测试台脚手架。
类似地，pnmake 和基于 IPC 的测试集将永不融入 /trunk ，但将成为新一代 Makefile::Parser 的 Nmake 部分的原型。
该分支从 Makefile::DOM 0.3.x 起启用。
Makefile::Parser
历史遗留的旧实现
Makefile::Parser 一年多以前发布在 CPAN 上的 0.11 版的旧实现仍将继续演化。其中的改进内容，主要包括：
整合 Adam Beauchamp 提供的基于状态机设计模式的补丁。
修复一个用户在 RT 中 报告的bug ，提供对 GNU make 函数引用的支持。
简单介绍新一代 Makefile::Parser 的开发现状和蓝图。
这些将以 0.xx 的版本号发布到 CPAN。
全新版本的实现
全新的实现将基于 Makefile::DOM，并保持接口的向下兼容。由于旧实现同时支持 GNU make 和 NMAKE 的常用语法，故要实现向后兼容，必须实现 Makefile 格式的自动识别。最简单的做法也许是先尝试用 Makefile::Parser::Gmake 进行处理，如果出现错误，就改用 Makefile::Parser::Nmake. 至于该做法的实际效果如何，只有留待实践的检验了。
基于 CPAN 发布的版本号的里程碑列表如下：
1.0.x_01
它们将整合 Makefile::DOM 的 /branches/gmake 分支的实现。版本号中的 _01 后缀将之标识为``Developer Release''；一般的 CPAN 升级工具将会忽略这样的发布，从而不致于突然破坏向下兼容。
1.1.x_01
它们将整合 Makefile::DOM 的 /branches/nmake 分支的实现代码。
1.2.x
它们将首次实现向下兼容，从而是 1.0.0_01 以来第一批 CPAN 正式发布版。
1.3.x
该系列将致力于把基于 IPC 的测试集转换为非 IPC 的版本，从而提高效率，增加可移植性。关于测试集可移植性的一个关键子项目是 Bourne Shell 的仿真。毕竟像 Win32 这样的平台，/bin/sh 一般是没有的。
Makefile::Parser 的 SVN 仓库位于：
http://svn.openfoundry.org/makefileparser/
未来该仓库将像 Makefile::DOM 那样分为 trunk 和若干个 branches.
Makefile::GraphViz
与 Makefile::Parser 类似，CPAN 上已有的 Makefile::GraphViz 实现将以 0.xx 的形式继续演化一段时间。这些发布将着力解决 Ken Williams 于几周前报告的那个有关 plot_all 方法的 bug:
http://rt.cpan.org/Ticket/Display.html
从 1.00 开始，它将使用 Makefile::Parser 1.2.x 及其以上版本。
Makefile::Compiler
该模块将支持 GNU make 和 MS NMAKE 两种格式的 Makefile 作为输入；输出将支持 Java 的 ANT，CPAN 上的 PBS，以及 GNU make 和 NMAKE 自身。该模块在早期将从 Makefile::Parser 产生的 AST 发射目标代码。该做法实现起来非常简单，虽然无法得到很``地道''的翻译，但却是``足够好的''。
有关该模块的计划目前无法确定下来，因为它强烈地依赖前几个模块的成果和经验。
07 febbraio
该项目将由下列三部分组成：
Makefile::DOM 该模块将 Makefile 视为“文档”进行“无损”的解析，生成类似 DOM 的树形结构。DOM 树中将保留原输入文件中的所有信息，包括空格、空行、注释等。这意味着，从 DOM 树可以还原出原始的 Makefile 文件。另外 DOM 树自身的每个节点甚至整体都是可修改的，就像 PPI 和 HTML::TreeBuilder 那样。
Makefile::DOM 的接口完全模仿了 PPI 的 API 设计。事实上，我直接照搬了 PPI::Node , PPI::Element , PPI::Dumper 的源代码和 POD 文档（此举已得到 PPI 的作者 Adam Kennedy 的完全许可）。
Makefile::DOM 被设计成与具体的 Makefile 语法无关。同一套 DOM 节点类型将在不同格式的 Makefile DOM 生成器之间共享，比如， MDOM::Document::Gmake 负责对 GNU Makefile 进行解析，返回 MDOM::Document 类的实例（即 DOM 树的根）；而 NMAKE Makefile 的解析器 MDOM::Document::Nmake 亦返回 MDOM::Document 类的实例。日后，还将考虑添加对 dmake 和 bsdmake 的支持。
目前 MDOM::Document::Gmake 已初具雏形，下面要做的就是添加遗漏的节点类型和进行综合测试。
测试 Makefile::DOM 最好的方法就是在其基础之上，开发出完整的 make 工具，然后通过对应 make 工具的测试集。比如，测试 MDOM::Document::Gmake 最好的方法就是利用它实现一个 pgmake 脚本，然后去跑 GNU make 官方测试集。类似地，我也需要开发出 pnmake 脚本。
Makefile::Parser 全新的 Makefile::Parser 实现不会在 API 上进行太大的改动。换言之，新版本的接口仍将基本按照 0.11版 也即 Make 模块的接口来设计。尽管如此，我仍会根据需要，对 API 进行扩展和补充。
Makefile::Parser 的任务在于，从 make 工具的视角，对 Makefile DOM 树进行深层的语法分析和语义脱糖。这意味着，得到的 AST 必然是“有损”的，而且必然包含了当前环境中的信息。这些环境信息包括系统中的环境变量设置、命令行选项、命令行传递的 Makefile 变量值、甚至磁盘文件的当前状态等。这种环境信息的依赖意味着 Makefile::Parser 并不适合进行严格意义上的 Makefile 翻译与转换工作。真正的翻译与转换要求 AST 是与上下文无关的，因此必须从 Makefile::DOM 出发重新开始。
Makefile::Parser 的用途很多，比如对 Makefile 中的依赖关系进行可视化（典型的应用就是 Makefile::GraphViz 这样的模块）。另外就是进行一些实用主义的翻译。当需要转换的 Makefile 并未使用强烈依赖于上下文的高级特性的时候，从 Makefile::Parser 产生的 AST 出发已经可以得到相当令人满意的翻译了。
Makefile::GraphViz 下一代的 Makefile::GraphViz 将基于 Makefile::DOM 和全新的 Makefile::Parser ，同时保持向后兼容。
Makefile::Compiler 该模块就是进行不同格式 Makefile 之间的转换，以及将某一种格式的 Makefile 转换成其他非 make 项目管理工具的配置文件，比如 PerlBuildSystem, Rake, 和 Ant.
正如前面提到的，这里最简单的做法就是从 Makefile::Parser 生成的“有损” AST 出发，进行代码生成。但是通过这种方式得到的目标代码强烈地依赖于进行翻译时刻的系统上下文，影响目标代码的通用性和可移植性。尽管如此，对于许多足够简单的 Makefile 而言，种用这种方法生成的目标代码已经足够好了。幸运的是，现实世界中的大部分 Makefile 都是足够简单的。
更完美的翻译方式当然是从最底层的 DOM 树出发，按照类似“程序形式化证明”的方法进行复杂的 AST 变换。利用此种手段可以得到相当“地道“的目标代码，其质量接近人类手写的代码，但是 AST 变换算法可能会极端复杂。届时可以考虑使用像属性文法这样的工具（Language::AttributeGrammar ）。
在实际翻译中，有一个很重要的问题就是如何处理 Makefile 中内联的 shell 命令。毕竟任何一个 Makefile 文件中都包含至少两种“语言”：Makefile 本身的记法，以及命令中的 Shell 记法。比如 GNU makefile 中的 cp, mv 在 NMAKE makefile 中就不应当出现。这意味着，Makefile::Compiler 可能还得实现一个 shell 转换器以完成不同 shell 之间的编译工作……
在大三上学期的时候，即 2005 年国庆前后，我正在为我的计算机组成的课程设计项目
Salent 准备
报告 用的素材。那时我就想到从 Salent 项目自身的
Makefile 自动生成项目的
构造流程图 。毕竟 Makefile 文件中已经包含了项目文件间的依赖关系，以及从各组依赖项生成对应目标的 Shell 命令。
在这个应用中，我需要一个 Makefile 解析器以及一个有向图的示意图生成器。至于后者，AT&T 免费的 GraphViz 库可以很好地胜任。至于前者，我进行了大量的网络搜索。我试用了 CPAN 上的 Make 模块，但它不能很好地支持 NMAKE 语法的 Makefile，于是我就针对 Salent 项目的 Makefile 所使用的特性，同时综合了 GNU make 的一些常用特性，自主开发了 Makefile::Parser 模块，并发布到 CPAN。
很快地，以 Makefile::Parser 为基础，我推出了从 Makefile 自动生成构造流程图的 Makefile::GraphViz 模块。
有趣的是，CPAN 上也有一个所谓的 GraphViz::Makefile 模块。和我的不同的是，该模块是基于前面提到的 Make 模块的。因此与我的库实际上构成了``竞争''关系。
在随后的几周内，我开始根据 GNU make 手册 ，向我的 Makefile::Parser 不断地添加新特性。但我很快发现，已有的框架变得越来越难于扩展，根本无法胜任 gmake 庞大的特性集。因此当 Makefile::Parser 0.11 发布之后，我就放弃了旧的代码基础，开始另起炉灶了。
2006 年的冬天，我开始仔细阅读 GNU make 手册 ，并着手将 gmake 自身的测试集 移植到我自己的 Makefile::Parser 项目中来，以便采用测试驱动的方法来创建全新的 Makefile::Parser 实现。
虽然 gmake 官方的测试台亦是用 Perl 开发的，且亦可作用于任意的 make 可执行文件，但是它却使用的是过时的 Perl 4 语言，并大量调用了 sh, diff 等特定于 *NIX 的工具，从而变得高度不可移植。所以我才下决心使用现代的 Perl 5 自动化测试框架 Test::Base 对 gmake 已有的测试集进行改写，以期达到下列目标：
可以不加修改地运行在 Win32, Cygwin, FreeBSD, NetBSD, OpenBSD, Linux, Solaris, Mac OS X 等多种类型操作系统上。
测试用例采用声明性的记法，保证可读性、清晰性和简洁性。
易于扩展，并可用于编写针对其他 make 工具（如 nmake, dmake, bsdmake）的测试集
易于配置，可以指定任意的 shell 命令行作为 make 测试对象
为了确保新的 gmake 测试集的可移植性，我自己用纯 Perl 开发了一个 Bourne Shell 虚拟机 。毕竟，Windows 的 Shell 语法和行为与 Bourne Shell 是如此地不同。另外，其他系统中默认的 shell 也有可能是像 csh 这样的东西。由于该 sh 虚拟器是为 Makefile::Parser 的测试集服务的，因此只需要实现 Bourne Shell 特性的一个很小的子集，即 gmake 测试用例中实际使用到的特性集。
目前，gmake 测试集的转换工作正在进行中，您可以从下面的位置看到已完成转换的 gmake 测试脚本：
http://svn.berlios.de/svnroot/repos/makefileps/t/gnu/
从那以后，迫于江大日益繁重的课业负担，Makefile::Parser 一直进展缓慢。在过去的一年中，有许多人向我表达了各种各样有趣的需求，这驱使我不断地调整项目的设计与目标。
AT&T 用户 Billy Patton 向我表达了他的一个有趣的需求：他希望能通过编程方式，读取一个 Makefile 文件，然后进行一些修改，再写回磁盘。他说，他希望通过 GUI 菜单来帮助没有 Makefile 使用经验的用户来操纵 Makefile。这个需求意味着，读取 Makefile 的过程必须是``无损''的，即我的库不可以扔掉包括注释、空行在内的任何东西，同时我还必须提供相应的接口将修改过的 Makefile AST 写回磁盘，即提供一种 Makefile Writer。
Gurets Maxim 通过 CPAN RT 向我 传达了 这样一个需求：他希望看到 Makefile::Parser 拥有 GNUMake, NMake, BSDMake 等多个子类，从而能解析各种已知格式的 Makefile. 他认为现有的 Makefile::Parser 实现将 NMAKE 和 GNU make 的特性杂糅在一起的做法并不可取。我表示赞同，因为 NMAKE 和 gmake 在行为上有许多矛盾之处。
微软公司 Unix 互操作团队的 Madhuri Mandava 和 Pugs 团队的 Christopher Malon 更乐衷于看到将 NMAKE 的 Makefile 转换为 gmake 格式的 Makefile，或者相反。这种需求要普遍得多，毕竟有太多太多基于 Linux 的开源项目需要移植到 Win32，而 Makefile 的翻译往往是很重要的组成部分。比如我自己就曾经吃力地将 Judy 库 的 Makefile 翻译为 NMAKE 接受的版本－－唔，那可真是枯燥之极。
这个世界上除了 make 还有许多其他的项目构造和管理工具，比如 Ruby 世界里的 Rake ， Java 里的 Ant，以及 CPAN 上的 PerlBuildSystem (PBS) 。PBS 的作者之一，瑞典的 Nadim Khemir 和我一直保待着通信联系。他非常希望看到，gmake 等其他 make 工具的 Makefile 文件能通过我的 Makefile::Parser 或者类似的东西，自动地转换为 PBS 自己的配置文件 (pbsfile)。
在 Nadim Khemir 的大力推动下，我于大四上学期的前一两个月，启动了 Makefile::DOM 项目。该项目受 Adam Kennedy (Alias) 的 PPI 模块的启发，将 Makefile 视为“文档”而非程序进行解析，解析的结果是一棵类似 DOM 的树型数据结构。该项目由于能无损地对 Makefile 进行解析，故可以很好地满足前面 Billy Patton 等人的需求。从 DOM 树写回 Makefile 也是极容易的。同时 Makefile::DOM 亦可作为其他所有需求及应用的基础，因为它实际上完成的是 Makefile 的词法分析以及一部分简单的语法分析任务。
Makefile::DOM 的进展非常迅速，目前已经支持了 Gnu Makefile 的大部分语言结构。我以为至少 0.0.1 版已经可以在近期发布到 CPAN 了。
06 febbraio
KB - VRG 知识库简介
Agent Zhang (章亦春) <agentzh at gmail dot com >
Maintainer: Agent Zhang <agentzh at gmail dot com>
这篇文档将简要地介绍一下 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 在立几空间中的推理任务主要是将复杂的关系分解为基本关系，或者将基本关系合成为复杂关系。
向量是立体几何元素的抽象表示。从数学语义上讲，立几空间中的平面在向量空间中对应其“法向量”，而立几空间中的直线在向量空间中对应其“方向向量”。
向量空间中的关系演绎是整个证明系统的核心。VRG 正是通过从已有的向量关系推出新的向量关系，来间接地从已有的几何关系推出新的几何关系的。
在向量空间中仅讨论下列关系：
平行关系 例如
a <//> b 表示向量 a 与向量 b 平行。
垂直关系 例如
a <T> b 表示向量 a 与向量 b 垂直。
斜交关系 例如
a <X> b 表示向量 a 与向量 b 斜交。
目前，知识库使用了下列假设条件：
取消这两条基本假设虽然从逻辑上更加完整，但从实用性的角度上讲，将不可避免地使知识库中到处充斥着“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 源文件构成：
该文件定义了知识库中所使用的特殊的运算符，例如前缀 \ 和中缀 //.该文件为知识库中所有其他 .xclp 文件所包含。详情请参与 记法约定 .
例如前缀 \ 的定义如下：
prefix:<\> line 而中缀 // 的定义如下：
infix:<//> parallel
该文件定义了 VRG 的“预处理规则”。这些规则的主要工作是在立几空间内部进行关系演算，其目的在于将 project（投影）和 meet（相交）这样的复杂关系转换为平行、垂直之类的简单关系，同时为某些基本关系生成“同构异形体”，以简化后续的匹配工作。
具体说来，此文件包含下列几条规则：
当两个平面 alpha 和 beta 相交于直线 l 时，则 alpha 与 beta不平行，并且 l 同时在 alpha 和 beta 上.
#?alpha, #?beta, meet(?alpha, ?beta, ?l) 这儿的前缀问号(?)表示为变量，而非常量。
当两条直线 l 和 m 相交于一点时，则存在一个平面 alpha 使得 l 和 m都在 alpha 上，且 l 不平行于 m.
\?l, \?m, meet(?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) 若平面 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.
若平面 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 和 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 在高中数学课本中有如下定理是该向量规则的“特殊表现形式”：
若向量 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 若用户求证 a 与 b 在立几空间存在关系 R，且事实库中不存在该事实，则生成 pending 事实以指示该目标“未决”。
?a *[?R] ?b, ~exists(?a [?R] ?b) 若用户给定的有关 a 和 b 的一求证目标未决，且事实库中存在 a 与 b之间确定的某种关系，则生成 hint 事实，以提示用户。
pending(space-relation, ?, ?a, ?b), ?a [?R] ?b
除了上述规则之外，知识库中还收录了许多自检测规则，用于检测事实库内部的完整性。这些设施可以有效地检测出用户给定事实之间的冲突、知识库规则之间的冲突，以及其他形式的 VRG bug.
事实上，在 VRG 的早期，这些自检测规则确实捕捉到不少连题库测试台都未捕捉到的 bugs。
一条典型的自检规则如下：
\?l, #?alpha, ?l [on] ?alpha, ?l [~on] ?alpha 其含义是：一条直线要么在一个平面上，要不不在那个平面上。如果同时存在这两个事实，则生成 contradction 事实指示矛盾冲突的存在。
将完整性测试逻辑与系统自身的实现放在一起，在软件工程中称为 Design by contract (DBC).VRG 的实践表明，在基于规则的系统中实现 DBC 要比传统的命令式语言要方便和自然得多。
您总是可以从下面的 Subversion (SVN) 仓库取得最新版本的 VRG 知识库：
https://svn.berlios.de/svnroot/repos/unisimu/VRG/knowledge
Copyright 2006 by Agent Zhang (章亦春). All rights reserved.
the Overview manpage
Overview - VRG 专家系统概览
章亦春 <agentzh at gmail dot com >
计算机科学与通信工程学院 江苏大学
Maintainer: Agent Zhang <agentzh at gmail dot com>
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 描述自己的问题。
例如上面的第 1 题可以用 VRG 用户语言表达如下：
line l, m; 第 2 题可以表达如下：
plane alpha , beta ; line a , b ; alpha T beta, a T beta => a // alpha 第 3 题可以表达如下：
plane alpha, beta, theta; 第 4 题可以表达如下：
line l1 , l2 , l3 , l4 ; plane alpha , beta ; point P , Q ; l1 on alpha, l2 on alpha, meet(l1, l2, Q), 第 5 题可以表达如下：
plane alpha, beta; 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 作为文件扩展名。然后使用下面的命令行进行求解：
$ perl script/vrg-run.pl foo.vrg 典型地，若将上面的第 1 题用 VRG 语言描述后保存至 problem-1.vrg 文件，则运行 vrg-run 程序的情景如下：
$ perl script/vrg-run.pl problem-1.vrg generating vectorize.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 在内部使用 AT&T 的自由软件库 Graphviz 来生成所有的有向图。
对于多证明目标的题目，VRG 在判断不成立时，会显式地指出具体是哪些目标是未决的。而对于题目自身的条件是彼此冲突的，比如两个几何元素既平行又垂直了，VRG 也会显式地指出冲突所涉及的细节（比如哪两个元素冲突了，是哪两个关系冲突了）。
我已使用高中数学教材中所有的公理、定义、定理和推论对 VRG 进行了测试（在 VRG的测试集中即对应 sanity.t 文件），此外，我还使用高三时候积累的所有相关的高考复习题对 VRG 进行了测试（在测试集中即对应 senior.t 文件）。
对于涉及定量关系的几何问题是无法用 VRG 进行求解的，比如角度计算问题、线段长度之类。VRG 是定性求解系统，它只能处理“垂直”、“平行”、“线在面上”这样的定性关系。
VRG 的知识库全部是使用我自主设计和实现的通用目的专家系统编程语言 XClips 进行描述的，在 VRG 源代码目录中，对应 knowledge/*.xclp 这些文件。
由于使用了可扩展的 XClips 语言，VRG 的知识库非常简洁，非常清晰。
VRG 在底层使用了美国航空航天局约翰逊太空中心开发的正向链推理机 CLIPS. 事实上，VRG 系统与 CLIPS 的交互全部是通过 XClips 系统来完成的。XClips 正是建筑在CLIPS 之上的。
值得一提的是，CLIPS 是发布在公共域(public domain)中的，因此可以将之用于任何目的。
VRG 的构件和依赖项都是高度可移植的，包括 CLIPS, perl, Graphviz, 因此可以不加修改地运行在包括 Windows, Linux, FreeBSD, Solaris 在内的多种操作系统上。目前，我只在 Windows XP 和 Windows 2000 上进行过测试。
您总是可以从下面的 SVN 仓库获得 VRG 最新版本的源代码：
http://svn.berlios.de/svnroot/repos/unisimu/VRG
如果您想帮助完善 VRG 系统，请发送电子邮件告知作者。谢谢！
Copyright 2006 by Agent Zhang (章亦春). All rights reserved.
the KB manpage
Strumenti 
