命题逻辑以简单命题为最小单位，研究由简单命题和联结词构成的复合命题的逻辑性质以及关于复合命题之间的推理关系。命题逻辑中有很多个形式推理系统，本文讨论的形式推理系统是重言式系统。由重言式系统的可靠性和完备性可知，重言式系统中内定理等价于重言式。在命题逻辑中，重言式的判定问题已经得到解决，有基于语法或语义的算法提出，因而重言式系统中内定理的判定问题已经得到解决。但在重言式系统中内定理的证明必须给出严格的证明序列，而这种证明往往依赖于经验和技巧，到现在为止这个问题都没有很好的解决办法，它仍然是困扰着数理逻辑学习者的难题。本文从机器证明的角度来对这个问题进行探讨，希望能够实现内定理证明序列的自动生成。 本文提出了基于演绎定理进行重言式系统中内定理证明的方法，该方法使用演绎定理将内定理的证明与有前提的证明结合起来，把对公理和规则的使用简化为推理过程中的推理规则，并适当的引入内定理丰富推理规则从而简化推理的过程，而序列填充的过程则采取了构造性的方法。该方法的具体处理流程是：先使用判定算法判定待证的公式是否是内定理，在确定了公式是内定理后利用演绎定理把对该公式的证明转化为有前提的证明，证明过程使用本文提出的推理规则进行推理(去除否定联结词或对结论进行细化会引起结论的转换)获取证明序列，在得到证明序列后通过机械填充的方式转化成符合要求的证明序列。 本文对该方法进行了系统实现，并对参考文献中关于重言式系统P的习题和提出的定理和命题成功地进行了证明。尽管本方法并不具备完全性，但实践表明该方法有着很好的应用效果，为重言式系统中内定理证明的难题提供了一个比较有效的解决方案。