摘要
本文后其后续文章将系统地探讨中介逻辑诸子系统的自动推理理论及其实现方式。本文着重讨论中介命题逻辑的自动定理证明理论。文中给出了中介命题逻辑ＭＰ及ＭＰ的表推演系统，证明了该系统的可靠性与完备性，并给出利用这一理论实现ＭＰ与ＭＰ系统定理自动证明的算法。
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.
出处
《模式识别与人工智能》
EI
CSCD
北大核心
1994年第2期87-93,共7页
Pattern Recognition and Artificial Intelligence
基金
国家高技术研究发展计划资助项目(863-306-O5-16B)
关键词
自动定理证明
中介逻辑
表推演方法
Automated Theorem Proving, Medium Logic, Tableau Method.
