Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.

翻译：基于归约排序的重写技术生成“恰到好处”的推论，以保持一阶完备性。这对于基于叠加的一阶定理证明而言是理想的，但针对至少一种归纳推理方法，我们发现遗漏了关键的推论。因此，我们扩展了叠加演算，引入基于重写的技术来生成足够推论，以实现饱和过程中的归纳自动化。当将我们的工作应用于单位等式片段时，使用定理证明器Vampire进行的实验表明，归纳推理性能得到了显著提升。