Automation of inductive theorem proving in equational logic with multi-context reasoning

自动归纳定理证明是验证软件系统正确性的一项重要技术，本文研究了自动归纳定理证明的有效过程和推理策略。首先，我们提出了一种多上下文推理的证明方法，该方法可以同时执行一些不同推理策略中常见的推理。其次，我们提出了在归纳定理证明中经常需要的正确引理的生成原则。

We have studied on the efficient procedure and reasoning strategy for automating inductive theorem proving, which is an important technique for verifying correctness of software systems. First, we proposed a proof method with multi-context reasoning, which can perform inferences commonly appearing in some different reasoning strategies simultaneously. Second, we proposed a principle for generating correct lemmas which are often required in inductive theorem proving.