中介自动推理的理论与实现（Ⅲ）——中介逻辑定理证明器

摘要

文[1]、[2]建立了中介逻辑的表推演理论,本文着重介绍以这一理论为基础设计的实验性中介逻辑定理证明器（MTP）。这一定理证明器能实现中介逻辑各子系统（包括经典一阶逻辑）中定理的自动证明。文中介绍了MTP采用的基本算法、基本结构及技术途径。