Superposition modulo linear arithmetic SUP(LA)
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4089320 (Why is no real title available?)
- scientific article; zbMATH DE number 1765672 (Why is no real title available?)
- scientific article; zbMATH DE number 1444363 (Why is no real title available?)
- Combining superposition, sorts and splitting
- Engineering DPLL(T) + Saturation
- Integrating Linear Arithmetic into Superposition Calculus
- New results on rewrite-based satisfiability procedures
- Refutational theorem proving for hierarchic first-order theories
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
Cited in
(28)- Generalized rewrite theories, coherence completion, and symbolic methods
- The QSMA algorithm for quantifiers in SMT
- An efficient subsumption test pipeline for BS(LRA) clauses
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Hierarchic superposition revisited
- A superposition calculus for abductive reasoning
- Harald Ganzinger's legacy: contributions to logics and programming
- Combining superposition and induction: a practical realization
- On deciding satisfiability by theorem proving with speculative inferences
- Superposition for bounded domains
- Hierarchic superposition with weak abstraction
- Layered clause selection for theory reasoning (short paper)
- Superposition modulo a Shostak theory.
- Making higher-order superposition work
- On First-Order Model-Based Reasoning
- Theorem proving in large formal mathematics as an emerging AI field
- Making higher-order superposition work
- Making theory reasoning simpler
- Rewriting modulo SMT and open system analysis
- Superposition modulo non-linear arithmetic
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Superposition as a decision procedure for timed automata
- Superposition decides the first-order logic fragment over ground theories
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Model Evolution with Equality Modulo Built-in Theories
- Linear quantifier elimination as an abstract decision procedure
- ALASCA: reasoning in quantified linear arithmetic
- Integrating Linear Arithmetic into Superposition Calculus
This page was built for publication: Superposition modulo linear arithmetic SUP(LA)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3655193)
