# Subsumption Demodulation in First-Order Theorem Proving

arXiv: https://arxiv.org/abs/2001.10213 · HTML: https://mlsanity.com/paper/2001.10213/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Jan 2020.

## Built on by (most cited first, 1 of 1)

- [An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction](https://mlsanity.com/paper/2511.04092/) (2025)

## Abstract (arXiv)

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.