Dr. Marco Voigt

Research Scientist

 

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

+49 681 9325-2917, fax -2999

mvoigt@mpi-inf.mpg.de, 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.
We have found decidable extensions of the Bernays-Schönfinkel-Ramsey fragment of first-order logic (E*A* prefix sentences) combined with restricted constraints on real-valued variables. Apart from the theoretical aspects of these results, we have put particular emphasis on decision procedures that behave well in practice.
In first-order logic without a-priori-interpreted symbols we have described novel decidable fragments that generalize many well-known decidable fragments (cf. the figure below), including several prefix fragments, several guarded fragments, the two-variable fragment, and the fluted fragment. The syntactic criteria for the novel fragments restrict the way of how certain first-order variables may co-occur in atoms — we speak of separated variables in this context. Details can be found in my PhD thesis (PDF / PDF with hyperref; via DOI: 10.22028/D291-28428).
Old (left-hand side) and novel (right-hand side) decidable fragments of first-order logic
My research was partially supported by the German Transregional Collaborative Research Center SFB/TR 14 AVACS in 2014 and 2015.

Education

  • since November 2013:
    Member of the group Automation of Logic at the Max Planck Institute for Informatics
  • July 2019:
    PhD in Computer Science at Saarland University, Saarbrücken, Germany
    Dissertation: Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates
    (PDF / PDF with hyperref; via DOI: 10.22028/D291-28428)
  • October 2012 - July 2019:
    PhD 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

Teaching

Summer 2019:
  • Lecturer for Decision Procedures with Christoph Weidenbach, Max Planck Institute for Informatics, Saarbrücken
Winter 2013/14:
  • Teaching assistance for Automated Reasoning by Uwe Waldmann, Max Planck Institute for Informatics, Saarbrücken
Winter 2012/13:
Summer 2012:
Winter 2011/12:

Publications and selected talks

  • Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates
    PhD thesis (submitted in February 2019, defended on July 31 2019)
    PDF without hyperref / PDF with hyperref
    Thesis via DOI: 10.22028/D291-28428
  • 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): 10.1007/978-3-030-29007-8_2
    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)