Integrating Linear Arithmetic into Superposition Calculus

DOI10.1007/978-3-540-74915-8_19zbMath1179.03018OpenAlexW1557130751MaRDI QIDQ3608415

Andrei Voronkov, Konstantin Korovin

Publication date: 5 March 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74915-8_19

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Related Items (16)

Lemmaless induction in trace logic ⋮ Superposition as a decision procedure for timed automata ⋮ Superposition decides the first-order logic fragment over ground theories ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ SMELS: Satisfiability Modulo Equality with Lazy Superposition ⋮ Engineering DPLL(T) + Saturation ⋮ Making theory reasoning simpler ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Linear Quantifier Elimination as an Abstract Decision Procedure ⋮ Combinable Extensions of Abelian Groups ⋮ Interpolation and Symbol Elimination ⋮ Model Evolution with Equality Modulo Built-in Theories ⋮ Superposition Modulo Linear Arithmetic SUP(LA) ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ SMELS: satisfiability modulo equality with lazy superposition

This page was built for publication: Integrating Linear Arithmetic into Superposition Calculus