- Formal logics and reasoning, in particular:
- decidable fragments of first-order logic
- decidable combinations of first-order fragments and fragments of background theories
In the Automation of Logics Group, my research mainly focuses on identifying new decidable fragments of first-order logics, possibly combined with fragments of linear arithmetic over the reals.
First results concern the Bernays-Schönfinkel-Ramsey fragment of first-order logic combined with restricted constraints on real-valued variables. Apart from the theoretical aspects of these results, we've put particular emphasis on developing techniques that facilitate efficient decision procedures. To this end, we successfully employ techniques inspired by quantifier elimination methods for linear real arithmetic.
In the field of pure first-order logic we have described novel fragments that generalize classical fragments which have been known for long, such as the monadic fragment, the Bernays-Schönfinkel-Ramsey fragment, and the Ackermann fragment. The syntactic criteria of the novel fragments do neither refer to the arity of predicate symbols nor to particular quantifiers prefixes. We rather restrict the way of how differently quantified variables may occur together in atoms.
My research was partially supported by the German Transregional Collaborative Research Center SFB/TR 14 AVACS in 2014 and 2015.
- since November 2013:
Member of the group Automation of Logic at the Max Planck Institute for Informatics
- since October 2012:
Ph.D. candidate at the Saarbrücken Graduate School of Computer Science at Saarland University, Saarbrücken, Germany
- May 2012:
Diploma in Computer Science (with distinction) at Dresden University of Technology, Dresden, Germany
Final thesis: On Polymorphic Types with Enforceable Linearity for a Quantum Lambda Calculus (PDF)
Thesis supervisor: Dr. Monika Sturm (Chair of Automata Theory, headed by Prof. Dr.-Ing. Franz Baader)
- September 2009 - February 2010:
Erasmus exchange student at Masaryk University, Brno, Czech Republic
- October 2005 - May 2012:
Studies in Computer Science at Dresden University of Technology, Dresden, Germany
- Teaching assistance for Automated Reasoning by Uwe Waldmann, Saarland University
- Teaching assistance for Grundzüge der theoretischen Informatik by Wolfgang J. Paul, Saarland University
- Teaching assistance for Theoretische Informatik und Logik by Christel Baier and Steffen Hölldobler, TU Dresden
- Teaching assistance for Formale Systeme by Christel Baier, TU Dresden
I was the elected representative of our institute's Ph.D. candidates from August 2014 until June 2016.
In July 2016 Mohamed Omran took over the position.
Visit our internal PhDrep page for more information.
Publications and selected talks
- Towards Elimination of Second-Order Quantiers in the Separated Fragment.
Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017).
Paper (CEUR Workshop Proceedings Vol-2013): PDF
- The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable.
11th International Symposium on Frontiers of Combining Systems (FroCoS 2017).
Paper (via DOI): 10.1007/978-3-319-66167-4_14
Extended preprint version: arXiv:1706.08504, 2017.
- On Implicit Dependence and Independence between Differently Quantified First-Order Variables.
Computer Science Logic (CSL 2017) short talk.
- On Generalizing Decidable Standard Prefix Classes of First-Order Logic.
Preprint: arXiv:1706.03949, 2017.
Poster (presented at FroCoS 2017): PDF
- On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic.
(with Matthias Horbach and Christoph Weidenbach).
26th International Conference on Automated Deduction (CADE-26).
Paper (via DOI): 10.1007/978-3-319-63046-5_6
Extended preprint version: arXiv:1705.08792, 2017.
- A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment.
32nd ACM/IEEE Symposium on Logic in Computer Science (LICS 2017).
Paper (via DOI): 10.1109/LICS.2017.8005094
Extended preprint version: arXiv:1704.02145, 2017.
- A fine-grained hierarchy of complete problems in the separated fragment of first-order logic.
Workshop Algorithmic Model Theory (AlMoTh 2017).
- The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable.
(with Matthias Horbach and Christoph Weidenbach).
Preprint: arXiv:1703.01212, 2017.
- Beyond Standard Miniscoping.
- The Complexity of Satisfiability in the Separated Fragment — A Journey Through ELEMENTARY and Beyond.
Sixteenth International Workshop on Logic and Computational Complexity (LCC2016).
- Deciding First-Order Satisfiability when Universal and Existential Variables are Separated.
(with Thomas Sturm and Christoph Weidenbach). 31st ACM/IEEE Symposium on Logic in Computer Science (LICS 2016).
Paper (via DOI): 10.1145/2933575.2934532
Extended preprint version: arXiv:1511.08999, 2016.
- Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete.
(with Christoph Weidenbach).
Preprint: arXiv:1501.07209, 2015.
- Lower Bounds for the Runtime of a Global Multi-Objective Evolutionary Algorithm.
(with Benjamin Doerr and Bojana Kodrič). IEEE Congress on Evolutionary Computation (CEC 2013).
Paper (via DOI): 10.1109/CEC.2013.6557601
- On Polymorphic Types with Enforceable Linearity for a Quantum Lambda Calculus.
Diploma Thesis at Dresden University of Technology, May 2012. (PDF)