The QSMA algorithm for quantifiers in SMT

DOI10.1007/S10817-025-09727-8MaRDI QIDQ6957141zbMATH OpenFDO

Authors Maria Paola Bonacina, Stéphane Graham-Lengrand

Publication date 16 July 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-025-09727-8

zbMATH Keywords

satisfiability modulo theorysatisfiability modulo assignmentquantified satisfiabilityautomated reasoning in arithmetic

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Cites work

• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• A model-constructing satisfiability calculus
• An abstraction-refinement framework for reasoning with large theories
• Applying Linear Quantifier Elimination
• Bugs, moles and skeletons: symbolic reasoning for software development
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
• Conflict-driven satisfiability for theory combination: transition system and completeness
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Efficient E-Matching for SMT Solvers
• FMplex: a novel method for solving linear real arithmetic problems
• Hierarchic superposition with weak abstraction
• Integrating Linear Arithmetic into Superposition Calculus
• Interpolation and model checking for nonlinear arithmetic
• Linear quantifier elimination
• On Fourier's algorithm for linear arithmetic constraints
• On deciding satisfiability by theorem proving with speculative inferences
• QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Quantifier instantiation techniques for finite model finding in SMT
• Revisiting enumerative instantiation
• SMT-based model checking for recursive programs
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Simplify: a theorem prover for program checking
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Solving bitvectors with MCSAT: explanations from bits and pieces
• Solving non-linear arithmetic
• Solving quantified bit-vectors using invertibility conditions
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Superposition modulo linear arithmetic SUP(LA)
• Syntax-guided quantifier instantiation
• The complexity of linear problems in fields

This page was built for publication: The QSMA algorithm for quantifiers in SMT

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