Lower bounds for the runtime of a global multi-objective evolutionary algorithm. - Benjamin Doerr; Bojana Kodric; Marco Voigt (IEEE Congress on Evolutionary Computation, 2013)

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. - Marco Voigt; Christoph Weidenbach (CoRR, 2015)

Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. - Thomas Sturm 001; Marco Voigt; Christoph Weidenbach (LICS, 2016)

On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. - Matthias Horbach; Marco Voigt; Christoph Weidenbach (CADE, 2017)

The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable. - Marco Voigt (FroCoS, 2017)

A fine-grained hierarchy of hard problems in the separated fragment. - Marco Voigt (LICS, 2017)

Towards Elimination of Second-Order Quantifiers in the Separated Fragment. - Marco Voigt (SOQE, 2017)

The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. - Matthias Horbach; Marco Voigt; Christoph Weidenbach (CoRR, 2017)

On Generalizing Decidable Standard Prefix Classes of First-Order Logic. - Marco Voigt (CoRR, 2017)

On the Expressivity and Applicability of Model Representation Formalisms. - Andreas Teucke; Marco Voigt; Christoph Weidenbach (FroCos, 2019)

Separateness of Variables - A Novel Perspective on Decidable First-Order Fragments. - Marco Voigt (CoRR, 2019)

Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates. - Marco Voigt (2019)

Decidable ∃ *∀ * First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates. - Marco Voigt (J. Autom. Reason., 2021)