- formal logics and reasoning, in particular:
- decidable fragments of first-order logic
- decidable combinations of first-order fragments and fragments of background theories
- automata theory
- lambda calculi and type theory
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 has taken over the position.
Visit our internal PhDrep page for more information.
Publications and selected talks
- 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): coming soon.
Extended preprint version: coming soon.
- 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), pp. 432-439.
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)