符号计算系统设计与实现国际研讨会

文摘:本文介绍了一个基于共享内存多处理器的Grobner计算系统。其基本思想是，每个处理器从未约简的临界对集合中选择一个元素，约简与之相关的s多项式，并根据结果更新基和临界对集合。该算法的独创性在于它需要在进程之间进行少量的同步。文中给出了在16个处理器的Encore机器上实现的细节，以及使用文献中著名示例执行的测试结果。

文摘:我们正在构建一个通用工具，用于计算和可视化代数方程组的解。对于这个问题和相关的子问题存在不同的算法，我们将结合其中的几个算法。我们还开发了一套新的求解技术，使用任意代数集和超曲面之间的多多项式结果和双族映射。我们设计的工具应该是便携式的，并允许快速原型化新的和现有的算法，在一个智能混合代数和数值方法，以及实际的解决方案。复杂的解也可以计算出来，但是将它们可视化是困难的。该软件还应利用现有的任何并行硬件。总而言之，我们期望通过设计新技术，混合现有方法形成新方法，并比较各种方法的相对功效来改进代数方程求解的艺术状态。

文摘:规范语言TROLL light旨在用于信息系统的概念建模。它将话语宇宙(UoD)描述为一个同时存在并相互作用的对象系统，即一个对象共同体。

文摘:我们描述了一个已集成到代数数论系统Kant中的数字字段数据库。该数据库提供了对过去几年计算过的数字字段表的有效访问，并且易于扩展

文摘:Prolog技术定理证明程序(PTTP)是Prolog的一个扩展，它对于完整的一阶谓词演算是完整的。它与Prolog的不同之处在于，它统一使用了发生检验的稳稳性，深度优先迭代深化搜索代替了无界深度优先搜索，使搜索策略完整，并在Prolog推理中加入了模型消去约简规则，使推理系统完整。本文介绍了一种基于prolog的PTTP实现方法。它使用三个编译时转换，将公式转换为Prolog子句，这些子句在几个运行时谓词的支持下，直接执行带有深度优先迭代深化搜索的模型消除过程，并与发生检查相统一。它的高性能超过了基于prolog的PTTP解释器，并且比早期的基于lisp的编译器更简洁和可读，这使得它更适合于解释性目的。编译时转换的输入和输出示例提供了一种简单而精确的方式来解释PTTP是如何工作的。这个基于Prolog的版本更容易将PTTP定理证明思想合并到Prolog程序中。对Prolog的扩展提出了一些建议，可以用来提高PTTP的性能。