Satisfiability Checking meets Symbolic Computation (Project Paper)

Erika Abraham; John Abbott; Bernd Becker; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James Davenport; Matthew England; Pascal Fontaine; Stephen Forrest; Alberto Griggio; Daniel Kröning; Werner M. Seiler; Thomas Sturm

doi:10.48550/arXiv.1607.08028

Satisfiability Checking meets Symbolic Computation (Project Paper)

Erika Abraham, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kröning, Werner M. Seiler, Thomas Sturm

Research Institute for Symbolic Computation

Research output: Working paper and reports › Preprint

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.

Original language	English
Number of pages	15
DOIs	https://doi.org/10.48550/arXiv.1607.08028
Publication status	Published - 2016

Publication series

Name	CoRR - Computing Research Repository
Volume	abs/1607.08028

Fields of science

101 Mathematics
101001 Algebra
101005 Computer algebra
101009 Geometry
101012 Combinatorics
101013 Mathematical logic
101020 Technical mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.48550/arXiv.1607.08028

Cite this

Abraham, E., Abbott, J., Becker, B., Bigatti, A. M., Brain, M., Buchberger, B., Cimatti, A., Davenport, J., England, M., Fontaine, P., Forrest, S., Griggio, A., Kröning, D., Seiler, W. M., & Sturm, T. (2016). Satisfiability Checking meets Symbolic Computation (Project Paper). (CoRR - Computing Research Repository; Vol. abs/1607.08028). https://doi.org/10.48550/arXiv.1607.08028

@techreport{4ad9cf92e9ff46eab7af50af1b3770eb,

title = "Satisfiability Checking meets Symbolic Computation (Project Paper)",

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.",

author = "Erika Abraham and John Abbott and Bernd Becker and Bigatti, {Anna Maria} and Martin Brain and Bruno Buchberger and Alessandro Cimatti and James Davenport and Matthew England and Pascal Fontaine and Stephen Forrest and Alberto Griggio and Daniel Kr{\"o}ning and Seiler, {Werner M.} and Thomas Sturm",

year = "2016",

doi = "10.48550/arXiv.1607.08028",

language = "English",

series = "CoRR - Computing Research Repository",

type = "WorkingPaper",

}

TY - UNPB

T1 - Satisfiability Checking meets Symbolic Computation (Project Paper)

AU - Abraham, Erika

AU - Abbott, John

AU - Becker, Bernd

AU - Bigatti, Anna Maria

AU - Brain, Martin

AU - Buchberger, Bruno

AU - Cimatti, Alessandro

AU - Davenport, James

AU - England, Matthew

AU - Fontaine, Pascal

AU - Forrest, Stephen

AU - Griggio, Alberto

AU - Kröning, Daniel

AU - Seiler, Werner M.

AU - Sturm, Thomas

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://arxiv.org/abs/1607.08028

U2 - 10.48550/arXiv.1607.08028

DO - 10.48550/arXiv.1607.08028

M3 - Preprint

T3 - CoRR - Computing Research Repository

BT - Satisfiability Checking meets Symbolic Computation (Project Paper)

ER -

Satisfiability Checking meets Symbolic Computation (Project Paper)

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this