Development of Multi-Context Reasoning Infrastructural Systems for Algebraic Software

在被称为项重写系统的代数计算机软件领域，该项目成功地开发了一个新的基础结构推理系统，该系统有效地解决了许多问题。这些问题包括将程序转化为总是终止并输出唯一解的程序的完备化问题。还包括自动归纳定理证明证明程序所满足的关键属性。其关键技术是多上下文推理，它允许非常有效的模拟并行执行的多个进程使用特殊的数据结构称为节点和启发式搜索。

In the field of algebraic computer software called the term rewriting systems, this project has successfully developed a new infrastructural reasoning system which solves a lot of problems efficiently. The problems include the completion problems for transforming programs into those which always terminate and output the unique solution. Also included is the automated inductive theorem proving for proving crucial properties to be satisfied by programs. The key technology is the multi-context reasoning which allows very efficient simulation of parallel execution of multiple processes using the special data structure called nodes and heuristic search.