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

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.
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},
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
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},
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.
2020
arXiv:2003.05633 [bibtex]
@unpublished{DCNLRACCDSUCAC2020,
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},
pages = {41 Seiten},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2003.05633},
}×
[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, 41 Seiten, Elsevier Science, 2020. https://arxiv.org/abs/2003.05633
DOI fulltext PDF [bibtex]
@phdthesis{C2020,
title = {Cylindrical algebraic decomposition for nonlinear arithmetic problems},
author = {Gereon Kremer},
booktitle = {Aachener Informatik-Berichte},
volume = {2020-04},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-05913},
url = { https://publications.rwth-aachen.de/record/792185},
}×
[issue]
Gereon Kremer. Cylindrical algebraic decomposition for nonlinear arithmetic problems, PhD Thesis, RWTH Aachen University, Volume 2020-04 of Aachener Informatik-Berichte, 1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme, 2020.
DOI fulltext PDF [bibtex]
@misc{NOFPCRGEA2020,
title = {New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)},
author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {2752},
pages = {178-188},
type = {Invited Abstract},
year = {2020},
doi = {10.18154/RWTH-2021-09565},
url = { https://publications.rwth-aachen.de/record/833961},
}×
[issue]
Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract), Volume 2752 of CEUR Workshop Proceedings, 178-188, RWTH Aachen, 2020.
arXiv:2004.04034 [bibtex]
@unpublished{NOFPCRG2020,
title = {New Opportunities for the Formal Proof of Computational Real Geometry?},
author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks},
pages = {14 Seiten},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2004.04034},
}×
[issue]
Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry?, 14 Seiten, 2020. https://arxiv.org/abs/2004.04034
Show all