论文部分内容阅读
文[1]、[2]建立了中介逻辑的表推演理论,本文着重介绍以这一理论为基础设计的实验性中介逻辑定理证明器(MTP)。这一定理证明器能实现中介逻辑各子系统(包括经典一阶逻辑)中定理的自动证明。文中介绍了MTP采用的基本算法、基本结构及技术途径。
In [1], [2], the theory of table deduction of intermediary logic is established. This paper focuses on the experimental Mediator Logic Theorem Proof (MTP) based on this theory. This theorem prover can automatically prove the theorems in each subsystem of the intermediate logic, including the classical first-order logic. This paper introduces the basic algorithm used in MTP, the basic structure and technical approach.