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

Full work available at URL https://doi.org/10.1007/978-3-031-30823-9_33

zbMATH Keywords

automated reasoninglinear arithmeticquantified first-order logicSMTtheorem proving

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

• A model-constructing satisfiability calculus
• AC-KBO revisited
• An AC-compatible Knuth-Bendix order.
• AVATAR: The Architecture for First-Order Theorem Provers
• 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
• scientific article; zbMATH DE number 1303342 (Why is no real title available?)
• 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
• Satisfiability modulo theories and assignments
• Seventeen provers under the hammer
• Solving quantified linear arithmetic by counterexample-guided instantiation
• SPASS-SATT. A CDCL(LA) solver
• Unification with abstraction and theory instantiation in saturation-based reasoning

Cited in

(2)

• Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories
• A higher-order Vampire (short paper)

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)