$$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
From MaRDI portal
Publication:2817292
DOI10.1007/978-3-319-42547-4_3zbMath1344.68198arXiv1607.08028OpenAlexW2482086987WikidataQ59590561 ScholiaQ59590561MaRDI QIDQ2817292
Pascal Fontaine, Martin Brain, Bruno Buchberger, Anna Maria Bigatti, John Abbott, Werner M. Seiler, Alberto Griggio, Thomas Sturm, Daniel Kroening, Erika Ábrahám, Bernd Becker, Alessandro Cimatti, Stephen Forrest, Matthew England, James H. Davenport
Publication date: 30 August 2016
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1607.08028
symbolic computationcomputer algebra systemssatisfiability modulo theoriessatisfiability checkinglogical problems
Related Items
Targeted configuration of an SMT solver, Computing with Tarski formulas and semi-algebraic sets in a web browser, Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT, What does ``without loss of generality mean, and how do we detect it, Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Using machine learning to improve cylindrical algebraic decomposition, Efficiently and effectively recognizing toricity of steady state varieties, The SAT+CAS method for combinatorial search with applications to best matrices, Editorial: Symbolic computation and satisfiability checking, Cylindrical algebraic decomposition with equational constraints, From simplification to a partial theory solver for non-linear real polynomial constraints, Applying computer algebra systems with SAT solvers to the Williamson conjecture, Satisfiability checking and symbolic computation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Real quantifier elimination is doubly exponential
- Comprehensive Gröbner bases
- The Magma algebra system. I: The user language
- Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Building Bridges between Symbolic Computation and Satisfiability Checking
- Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
- Computing cylindrical algebraic decomposition via triangular decomposition
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
- Solving Non-linear Arithmetic
- Satisfiability of Non-linear (Ir)rational Arithmetic
- Mathematics by machine
- Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation)
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- Linear Integer Arithmetic Revisited
- Simplification by Cooperating Decision Procedures
- QEPCAD B
- The Strategy Challenge in SMT Solving
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Real World Verification
- Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas
- The MathSAT5 SMT Solver
- The Problem of Integration in Finite Terms
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Symbolic integration
- A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
- Truth table invariant cylindrical algebraic decomposition
