Publication:2817292: Difference between revisions
From MaRDI portal
Publication:2817292
Created automatically from import240129110113 |
(No difference)
|
Latest revision as of 18:04, 3 February 2024
DOI10.1007/978-3-319-42547-4_3zbMATH Open1344.68198DBLPconf/mkm/AbrahamABBBBCDE16arXiv1607.08028OpenAlexW2482086987WikidataQ59590561 ScholiaQ59590561MaRDI QIDQ2817292FDOQ2817292
Pascal Fontaine, Martin Brain, Bruno Buchberger, Anna M. Bigatti, John Abbott, Werner M. Seiler, Alberto Griggio, Thomas Sturm, Daniel Kroening, Erika Ábrahám, Bernd Becker, Alessandro Cimatti, James H. Davenport, Stephen Forrest, Matthew England
Publication date: 30 August 2016
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Abstract: Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified SC-square community.
Full work available at URL: https://arxiv.org/abs/1607.08028
symbolic computationsatisfiability modulo theoriessatisfiability checkingcomputer algebra systemslogical problems
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Magma algebra system. I: The user language
- QEPCAD B
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- The MathSAT5 SMT Solver
- Computing cylindrical algebraic decomposition via triangular decomposition
- Simplification by Cooperating Decision Procedures
- Satisfiability of Non-linear (Ir)rational Arithmetic
- 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
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Solving Non-linear Arithmetic
- Real World Verification
- Comprehensive Gröbner bases
- The Problem of Integration in Finite Terms
- Real quantifier elimination is doubly exponential
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas
- Truth table invariant cylindrical algebraic decomposition
- Symbolic integration
- Building bridges between symbolic computation and satisfiability checking
- Linear Integer Arithmetic Revisited
- A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
- Mathematics by machine
- Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
- The Strategy Challenge in SMT Solving
- Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation)
Cited In (15)
- Editorial: Symbolic computation and satisfiability checking
- Using machine learning to improve cylindrical algebraic decomposition
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- Satisfiability checking and symbolic computation
- Cylindrical algebraic decomposition with equational constraints
- Targeted configuration of an SMT solver
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Efficiently and effectively recognizing toricity of steady state varieties
- Computing with Tarski formulas and semi-algebraic sets in a web browser
- The SAT+CAS method for combinatorial search with applications to best matrices
- Recent developments in real quantifier elimination and cylindrical algebraic decomposition (extended abstract of invited talk)
- What does ``without loss of generality mean, and how do we detect it
- Applying computer algebra systems with SAT solvers to the Williamson conjecture
- From simplification to a partial theory solver for non-linear real polynomial constraints
- Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT
Uses Software
This page was built for publication: $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2817292)
