ALASCA: reasoning in quantified linear arithmetic

DOI10.1007/978-3-031-30823-9_33MaRDI QIDQ6535381zbMATH OpenFDO

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

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

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)

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

Cites work

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

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)