Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification (Extended Version)

EasyChair Preprint 16032

Abstract

The calculus ALASCA extends superposition-based saturation proving with reasoning in
Uninterpreted Functions and Linear Real Arithmetic (UFLRA). As efficiency of saturation algorithms depend on literal selection, simplification, and redundancy elimination, this paper improves reasoning in Uflra by introducing theory-specific notions and methods for all of these techniques. The implementation of these methods in the first-order theorem prover Vampire shows substantial gains in every tested benchmark category, solving a number of problems previously unsolved by any system.

Keyphrases: SMT, automated reasoning, first-order theorem proving, linear arithmetic, literal selection, real arithmetic, redundancy, simplification, superposition

@booklet{EasyChair:16032,
  author    = {Johannes Schoisswohl and Laura Kovács and Konstantin Korovin and Andrei Voronkov},
  title     = {Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification (Extended Version)},
  howpublished = {EasyChair Preprint 16032},
  year      = {EasyChair, 2026}}