Gereon Kremer

kremer
Email
gereon.kremer at cs.rwth-aachen.de
Phone
+49 241 80 21243
Address
Room 4228
Ahornstraße 55
D-52074 Aachen

Research Interests

  • SMT solving
  • Nonlinear real arithmetic
  • Cylindrical Algebraic Decomposition
  • Integer arithmetic

Teaching

2023
fulltext PDF [bibtex]
@conference{CACQ2023,
title = {Cylindrical Algebraic Coverings for Quantifiers},
author = {Gereon Kremer and Jasper Kurt Ferdinand Nalbach},
booktitle = {CEUR Workshop Proceedings},
volume = {3458},
pages = {9 Seiten},
type = {Conference Paper},
year = {2023},
url = { https://publications.rwth-aachen.de/record/956001},
}×
[issue] 		Gereon Kremer, Jasper Kurt Ferdinand Nalbach. Cylindrical Algebraic Coverings for Quantifiers, 7. International Workshop on Satisfiability Checking and Symbolic Computation (SC² 2022), Volume 3458 of CEUR Workshop Proceedings, 9 Seiten, 2023.
2021
DOI fulltext PDF [bibtex]
@article{D2021,
title = {Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
publisher = {Elsevier Science},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {119},
pages = {pages 100633},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jlamp.2020.100633},
url = { https://publications.rwth-aachen.de/record/816049},
}×
[issue] 		Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Journal of Logical and Algebraic Methods in Programming 119, pages 100633, Elsevier Science, 2021.
DOI [bibtex]
@conference{EFTLPSI2021,
title = {Extending the Fundamental Theorem of Linear Programming for Strict Inequalities},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Gereon Kremer},
publisher = {Association for Computing Machinery},
booktitle = {ACM Conferences},
pages = {313-320},
type = {Conference Paper},
year = {2021},
doi = {10.1145/3452143.3465538},
url = { https://publications.rwth-aachen.de/record/823081},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Gereon Kremer. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities, International Symposium on Symbolic and Algebraic Computation (ISSAC '21), ACM Conferences, 313-320, Association for Computing Machinery, 2021.
DOI arXiv:2108.05320 [bibtex]
@unpublished{PUSTCQFNLRA2021,
title = {Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
pages = {5 Seiten},
type = {Preprint},
year = {2021},
doi = {10.48550/ARXIV.2108.05320},
url = { https://arxiv.org/abs/2108.05320},
}×
[issue] 		Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic, 5 Seiten, 2021. https://arxiv.org/abs/2108.05320
DOI arXiv:2109.01585 [bibtex]
@unpublished{OM2021,
title = {On the proof complexity of MCSAT},
author = {Gereon Kremer and Erika Ábrahám and Vijay Ganesh},
type = {Preprint},
year = {2021},
doi = {10.48550/ARXIV.2109.01585},
url = { https://arxiv.org/abs/2109.01585},
}×
[issue] 		Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the proof complexity of MCSAT, 2021. https://arxiv.org/abs/2109.01585
DOI [bibtex]
@conference{OICACSMTS2021,
title = {On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving},
author = {Gereon Kremer and Erika Ábrahám and Matthew England and James H. Davenport},
publisher = {IEEE},
pages = {37-39},
type = {Conference Paper},
year = {2021},
doi = {10.1109/SYNASC54541.2021.00018},
url = { https://publications.rwth-aachen.de/record/846648},
}×
[issue] 		Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving, 23. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 37-39, IEEE, 2021.
Show all