ALASCA: reasoning in quantified linear arithmetic

DOI10.1007/978-3-031-30823-9_33zbMATH Open1543.68406MaRDI QIDQ6535381FDOQ6535381

Authors: Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov 

Publication date: 13 December 2023

Recommendations

• Superposition modulo linear arithmetic SUP(LA)
• Integrating Linear Arithmetic into Superposition Calculus
• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
• Hierarchic superposition revisited
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

zbMATH Keywords

SMTtheorem provingautomated reasoninglinear arithmeticquantified first-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Faster, higher, stronger: E 2.3
• Beagle -- a hierarchic superposition theorem prover
• Resolution theorem proving
• Satisfiability modulo theories and assignments
• A model-constructing satisfiability calculus
• Conflict Resolution
• Efficient E-Matching for SMT Solvers
• Extending reduction orderings to ACU-compatible reduction orderings
• Title not available (Why is that?)
• AVATAR: The Architecture for First-Order Theorem Provers
• Paramodulation-based theorem proving
• Ordered chaining calculi for first-order theories of transitive relations
• Integrating Linear Arithmetic into Superposition Calculus
• SPASS-SATT. A CDCL(LA) solver
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Implementing Superposition in iProver (System Description)
• AC-KBO revisited
• An AC-compatible Knuth-Bendix order.
• Seventeen provers under the hammer

This page was built for publication: ALASCA: reasoning in quantified linear arithmetic

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