Integrating Linear Arithmetic into Superposition Calculus

DOI10.1007/978-3-540-74915-8_19MaRDI QIDQ3608415zbMATH OpenOpenAlexFDO

Authors Konstantin Korovin, Andrei Voronkov

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)

Recommendations

• Superposition modulo linear arithmetic SUP(LA)
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Superposition and Model Evolution Combined
• Hierarchic superposition revisited
• A combined superposition and model evolution calculus

Cited in

(24)

• Superposition as a decision procedure for timed automata
• Superposition decides the first-order logic fragment over ground theories
• An efficient subsumption test pipeline for BS(LRA) clauses
• Making theory reasoning simpler
• SMELS: satisfiability modulo equality with lazy superposition
• Integration of linear arithmetic and goal-oriented resolution for software reasoning
• Superposition modulo non-linear arithmetic
• Integrating simplex with tableaux
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Engineering DPLL(T) + Saturation
• Superposition modulo linear arithmetic SUP(LA)
• On deciding satisfiability by theorem proving with speculative inferences
• Theorem proving in large formal mathematics as an emerging AI field
• Harald Ganzinger's legacy: contributions to logics and programming
• Combinable Extensions of Abelian Groups
• Interpolation and Symbol Elimination
• Model Evolution with Equality Modulo Built-in Theories
• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
• Linear quantifier elimination as an abstract decision procedure
• Lemmaless induction in trace logic
• QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
• Symbolic Model Construction for Saturated Constrained Horn Clauses
• ALASCA: reasoning in quantified linear arithmetic
• The QSMA algorithm for quantifiers in SMT

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608415)