Superposition Modulo Linear Arithmetic SUP(LA)

DOI10.1007/978-3-642-04222-5_5zbMath1193.03024OpenAlexW1550776561MaRDI QIDQ3655193

Ernst Althaus, Christoph Weidenbach, Evgeny Kruglov

Publication date: 7 January 2010

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04222-5_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Superposition Modulo Non-linear Arithmetic, Rewriting modulo SMT and open system analysis, On First-Order Model-Based Reasoning, 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, Making theory reasoning simpler, Superposition for Bounded Domains, Theorem Proving in Large Formal Mathematics as an Emerging AI Field, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, A superposition calculus for abductive reasoning, Linear Quantifier Elimination as an Abstract Decision Procedure, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Model Evolution with Equality Modulo Built-in Theories, Generalized rewrite theories, coherence completion, and symbolic methods, Layered clause selection for theory reasoning (short paper), An efficient subsumption test pipeline for BS(LRA) clauses

Cites Work

• Refutational theorem proving for hierarchic first-order theories
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Engineering DPLL(T) + Saturation
• Integrating Linear Arithmetic into Superposition Calculus
• New results on rewrite-based satisfiability procedures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item