Satisfiability Checking and Symbolic Computation [SC2]

Project Lead

Project Duration

01/07/2016 - 31/08/2018

Project URL

Go to Website

Partners

Publications

2018

Experiments with Automatic Proofs in Elementary Analysis

T. Jebelean

Technical report no. 18-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2018. Work in progress. [pdf] [zip] [pdf]
[bib]
@techreport{RISC5692,
author = {T. Jebelean},
title = {{Experiments with Automatic Proofs in Elementary Analysis}},
language = {english},
abstract = {Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non--clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms.We demonstrate on some concrete examples several heuristic techniques for the automation of natural--style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra.Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions.These techniques are being implemented in the {\em Theorema} system and are able to construct automatically natural--style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.},
number = {18-06},
year = {2018},
month = {April},
keywords = {Satisfiability Checking, Natural-style Proofs, Symbolic Computation},
sponsor = {European project ``Satisfiability Checking and Symbolic Computation'' (H2020-FETOPN-2015-CSA 712689)},
length = {33},
type = {Work in progress},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

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…