Download PDFOpen PDF in browser

Reducibility Constraints in Superposition

EasyChair Preprint no. 12142

27 pagesDate: February 15, 2024


Modern superposition inference systems aim at reducing the search space by introducing redundancy criteria on clauses and inferences. This paper focuses on reducing the number of superposition inferences with a single clause by blocking inferences into some terms, provided there were previously made inferences of a certain form performed with predecessors of this clause. Other calculi based on blocking inferences, for example basic superposition, rely on variable abstraction or equality constraints to express irreducibility of terms, resulting however in blocking inferences with all subterms of the respective terms. Here we introduce reducibility constraints in superposition to enable a more expressive blocking mechanism for inferences. We show that our calculus remains (refutationally) complete and present redundancy notions. Our implementation in the theorem prover Vampire demonstrates a considerable reduction in the size of the search space when using our new calculus.

Keyphrases: Reducibility constraints, redundancy, saturation, superposition

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Marton Hajdu and Laura Kovács and Michael Rawson and Andrei Voronkov},
  title = {Reducibility Constraints in Superposition},
  howpublished = {EasyChair Preprint no. 12142},

  year = {EasyChair, 2024}}
Download PDFOpen PDF in browser