Marco Voigt
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
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 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).
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 assistant for Automated Reasoning by Uwe Waldmann, Max Planck Institute for Informatics, Saarbrücken
Winter 2012/13:
- Teaching assistant for Grundzüge der theoretischen Informatik by Wolfgang J. Paul, Saarland University
Summer 2012:
- Teaching assistant for Theoretische Informatik und Logik by Christel Baier and Steffen Hölldobler, TU Dresden
Winter 2011/12:
- Teaching assistant for Formale Systeme by Christel Baier, TU Dresden
Publications and selected talks
- Separateness of Variables -- A Novel Perspective on Decidable First-Order Fragments
Submitted. Preprint: arXiv:1911.11500, 2019. - Decidable E*A* First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates
Submitted. 2019. - 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)