中介自动推理的理论与实现(Ⅱ)——中介谓词逻辑的表推演系统

THEORIES AND IMPLEMENTATIONS OF AUTOMATED REASONING IN MEDIUM LOGIC: (II)-TABLEAU SYSTEMS OF MEDIUM PREDICATE CALCULUS

本文以文（１）为基础，继续讨论中介逻辑的自动推理理论。文中给出了中介谓词演算系统ＭＦ及ＭＦ，带等词的中介词演算系统ＭＥ及ＭＥ的表推演系统，通过对表推演概念的扩充，详细证明了ＭＦ的表推演系统的可靠性与完备性，同时给出了其定理自动证明的理论算法。

This article is the second of a series of articles discussing theoretical and implementational problems on automated reasoning in medium logic. Based on article [I], we present tableau systems of medium predicate calculus MF and MF*, and medium predicate calculus with equality ME and ME*. We prove soundness and completeness of the tableau system of MF* in detail and give an theoretical algorithm of automated theorem proving for them.