Marco Voigt

Doctoral researcher


Max-Planck-Institut für Informatik
Saarland Informatics Campus
Campus E1 4
66123 Saarbrücken

+49 681 9325-2917, fax -2999, PGP


Physical address: building E1 5, room 636

Personal Information

Research Interests

  • Formal logics and reasoning, in particular:
    • decidable fragments of first-order logic
    • decidable combinations of first-order fragments and fragments of background theories
In general, I'm interested in formal logics and automated reasoning. The logics I'm interested in range from first-order to higher-order logics, including modal and temporal aspects, and also cover combinations of 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

Academic Activities


Winter 2013/14:
Winter 2012/13:
Summer 2012:
Winter 2011/12:

Publications and selected talks

  • On the Expressivity and Applicability of Model Representation Formalisms
    (with Andreas Teucke and Christoph Weidenbach).
    12th International Symposium on Frontiers of Combining Systems (FroCoS 2019).
    Paper (via DOI): TBA
    Extended preprint version: arXiv:1905.03651, 2019.
  • On Implicit Dependence and Independence between Quantified First-Order Variables.
    Workshop Algorithmic Model Theory (AlMoTh 2018).
    Slides: PDF
  • Towards Elimination of Second-Order Quanti ers in the Separated Fragment.
    Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017).
    Paper (CEUR Workshop Proceedings Vol-2013): PDF
    Slides: 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.
    Slides: PDF
  • On Implicit Dependence and Independence between Differently Quantified First-Order Variables.
    Computer Science Logic (CSL 2017) short talk.
    Slides: PDF
  • 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.
    Slides: PDF
  • 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.
    Slides: PDF
  • A fine-grained hierarchy of complete problems in the separated fragment of first-order logic.
    Workshop Algorithmic Model Theory (AlMoTh 2017).
    Slides: PDF
  • 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.
    Deduktionstreffen 2016.
    Slides: PDF
  • The Complexity of Satisfiability in the Separated Fragment — A Journey Through ELEMENTARY and Beyond.
    Seventeenth International Workshop on Logic and Computational Complexity (LCC 2016).
    Slides: PDF
  • 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.
    Slides: PDF
  • 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
    Slides: PDF
  • On Polymorphic Types with Enforceable Linearity for a Quantum Lambda Calculus.
    Diploma Thesis at Dresden University of Technology, May 2012. (PDF)