本文使用Ｃ—ＰＲＯＬＯＧ语言在ＳＵＮ工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统ＧＲＭ，ＲＭ，证明了《数学原理》中Ｐａｒｔ１：ｍａｔｈｅｍａｔｉｃａｌｌｏｇｉｃ中ＳｅｃｔｉｏｎＡ与ＳｅｃｔｉｏｎＢ中全部定理（３５０个）．讨论ＧＲＭ和ＲＭ的时、空复杂性，并在实现设计中提出新的全局调度策略及归结式的化简、排序策略，以单子句恒真、恒假的判断代替了广义归结中的自归结，实现了带ＯＣＣＵＲ检查的模式匹配． In this paper, C-PROLOG language is used to design and implement GRM, RM based on Generalized Summarization and Summarized Theorem on Sun workstation. It proves that all the theorems in Section A and Section B of Part 1: mathematicallogic in Mathematical Theory (350 ). This paper discusses the time and space complexity of GRM and RM, and puts forward a new global scheduling strategy and summary reduction and sorting strategy in the design of GRM. By replacing the judgment of general clause , A pattern match with OCCUR checking is achieved.