Subsumption Demodulation in First-Order Theorem Proving
Abstract
Motivated by applications of first-order theorem proving to software analysis, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning with conditional equalities in superposition-based theorem proving. We show that subsumption demodulation is a simplification rule that does not require radical changes to the underlying superposition calculus. We implemented subsumption demodulation in the theorem prover Vampire, by extending Vampire with a new clause index and adapting its multi-literal matching component. Our experiments, using the TPTP and SMT-LIB repositories, show that subsumption demodulation in Vampire can solve many new problems that could so far not be solved by state-of-the-art reasoners.
Keywords
Cite
@article{arxiv.2001.10213,
title = {Subsumption Demodulation in First-Order Theorem Proving},
author = {Bernhard Gleiss and Laura Kovacs and Jakob Rath},
journal= {arXiv preprint arXiv:2001.10213},
year = {2020}
}