Satisfiability Checking and Symbolic Computation [SC2]

Project Lead

Project Duration

01/07/2016 - 31/08/2018

Project URL

Project Website

Publications

2017

Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks

E. Abraham, T. Jebelean

In: ICAI 2017: 10th International Conference on Applied Informatics, G. Kusper (ed.), Proceedings of ICAI 2017: 10th International Conference on Applied Informatics, pp. 0-0. 2017. ISBN 0. In print. [url] [pdf]
[bib]
@inproceedings{RISC5546,
author = {E. Abraham and T. Jebelean},
title = {{Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks}},
booktitle = {{ICAI 2017: 10th International Conference on Applied Informatics}},
language = {English},
abstract = {We develop a case study on using quantifier elimination and cylindrical algebraic decomposition for the purpose of finding specific terms for the automation of proving mathematical properties in elementary analysis.Real--life proofs in specific mathematical domains are difficult to automate because of the high number of assumptions necessary for the prover to succeed. In particular, in elementary analysis, it is allmost impossible to find automatically the appropriate terms for the instantiation of universal assumptions and for witnessing the existential goals. We aim at developing such proofs in natural style, in the frame of the{\em Theorema} system.Finding such terms is actually possible by using quantifier elimination (QE) based on cylindrical algebraic decomposition (CAD). However, the current straightforward approach lacks in efficiency, because several redundant calls may be necessary, and because the nature of the problem is slightly different.We study some natural--style proofs, the necessary special terms, and the corresponding usage of the QE/CAD, and identify specific techniques for adapting these algorithms in order to increase their efficiency.The experiments are performed partially in {\em Mathematica} and partially in {\tt SMT-RAT}, the latter used as ``white--box'', which allows to inspect the intermediate results and to adapt certain parts of the algorithms.},
pages = {0--0},
isbn_issn = {ISBN 0},
year = {2017},
note = {In print},
editor = {G. Kusper},
refereed = {yes},
length = {0},
conferencename = {ICAI 2017: 10th International Conference on Applied Informatics},
url = {https://icai.uni-eszterhazy.hu/}
}

2016

Stam's Identities Collection: A Case Study for Math Knowledge Bases

Bruno Buchberger

In: Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Gert-Martin Greuel, Thorsten Koch, Peter Paule and Andrew Sommese (ed.), pp. 437-442. 2016. Springer International Publishing, Cham, 978-3-319-42432-3. [url] [pdf]
[bib]
@inproceedings{RISC5324,
author = {Bruno Buchberger},
title = {{Stam's Identities Collection: A Case Study for Math Knowledge Bases}},
booktitle = {{Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings}},
language = {english},
pages = {437--442},
publisher = {Springer International Publishing},
address = {Cham},
isbn_issn = {978-3-319-42432-3},
year = {2016},
editor = {Gert-Martin Greuel and Thorsten Koch and Peter Paule and Andrew Sommese},
refereed = {no},
length = {6},
url = {http://dx.doi.org/10.1007/978-3-319-42432-3_55}
}

The GDML and EuKIM Projects: Short Report on the Initiative

Bruno Buchberger

In: Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Gert-Martin Greuel, Thorsten Koch, Peter Paule and Andrew Sommese (ed.), pp. 443-446. 2016. Springer International Publishing, Cham, 978-3-319-42432-3. [url] [pdf]
[bib]
@inproceedings{RISC5325,
author = {Bruno Buchberger},
title = {{The GDML and EuKIM Projects: Short Report on the Initiative}},
booktitle = {{Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings}},
language = {english},
pages = {443--446},
publisher = {Springer International Publishing},
address = {Cham},
isbn_issn = {978-3-319-42432-3},
year = {2016},
editor = {Gert-Martin Greuel and Thorsten Koch and Peter Paule and Andrew Sommese},
refereed = {no},
length = {4},
url = {http://dx.doi.org/10.1007/978-3-319-42432-3_56}
}

Satisfiability Checking meets Symbolic Computation (Project Paper)

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

CoRR abs/1607.08028, pp. -. 2016. -. [url] [pdf]
[bib]
@article{RISC5351,
author = {Erika Abraham and John Abbott and Bernd Becker and Anna Maria Bigatti and Martin Brain and Bruno Buchberger and Alessandro Cimatti and James H. Davenport and Matthew England and Pascal Fontaine and Stephen Forrest and Alberto Griggio and Daniel Kroening and Werner M. Seiler and and Thomas Sturm},
title = {{Satisfiability Checking meets Symbolic Computation (Project Paper)}},
language = {english},
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. },
journal = {CoRR},
volume = {abs/1607.08028},
pages = {--},
isbn_issn = {-},
year = {2016},
refereed = {yes},
length = {15},
url = {http://arxiv.org/abs/1607.08028}
}

Loading…