Satisfiability Checking and Symbolic Computation [SC2]
Project Lead
Project Duration
01/07/2016 - 31/08/2018Project URL
Go to WebsitePartners
EU
Publications
2018
[Jebelean]
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, Austria. ISSN 2791-4267 (online). April 2018. Work in progress. [zip] [pdf] [pdf]@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
2017
[Jebelean]
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]@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/}
}
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
[Buchberger]
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. [doi] [pdf]@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}
}
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}
}
[Buchberger]
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. [doi] [pdf]@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}
}
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}
}
[Buchberger]
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]@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}
}
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}
}
