2024/02/29 by Hajdu, Márton, Kovács, Laura, Rawson, Michael · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2402.19199
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.