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 (19)

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 ⋮ QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment ⋮ Symbolic Model Construction for Saturated Constrained Horn Clauses ⋮ 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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Superposition Modulo Linear Arithmetic SUP(LA)