Rewriting and Inductive Reasoning
<|reference_start|>Rewriting and Inductive Reasoning: 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.<|reference_end|>
@article{hajdu2024rewriting,
    title={Rewriting and Inductive Reasoning},
    author={M'arton Hajdu, Laura Kov'acs, Michael Rawson},
    journal={arXiv preprint arXiv:2402.19199},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.19199},
    primaryClass={cs.LO}
}