中介自动推理的理论与实现（Ⅰ）——中介命题逻辑的表推演系统

摘要

本文及其后续文章将系统地探讨中介逻辑诸子系统的自动推理理论及其实现方式。本文着重讨论中介命题逻辑的自动定理证明理论。文中给出了中介命题逻辑MP及MP*的表推演（tableau）系统,证明了该系统的可靠性与完备性,并给出了利用这一理论实现MP与MP*系统定理自动证明的算法。