Integrating Linear Arithmetic into Superposition Calculus

Abstract. We present a method of integrating linear rational arithmetic into superposition calculus for first-order logic. One of our main results is completeness of the resulting calculus under some finiteness assumptions.

• Type: Conference
• Year: 2007
• Where: CSL
• Authors: Konstantin Korovin, Andrei Voronkov
• Keywords: CSL 2007, Rational Arithmetic, Superposition Calculus, first-order Logic