Decidability Results for Saturation-Based Model Building. - Matthias Horbach; Christoph Weidenbach (CADE, 2009)

Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries. - Matthias Horbach; Christoph Weidenbach (CSL, 2009)

Disunification for Ultimately Periodic Interpretations. - Matthias Horbach (LPAR (Dakar), 2010)

Superposition for fixed domains. - Matthias Horbach; Christoph Weidenbach (ACM Trans. Comput. Log., 2010)

Saturation-based decision procedures for fixed domain and minimal model validity. - Matthias Horbach (2010)

Predicate Completion for non-Horn Clause Sets. - Matthias Horbach (CADE, 2011)

System Description: SPASS-FD. - Matthias Horbach (CADE, 2011)

Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants. - Deepak Kapur; Zhihai Zhang; Matthias Horbach; Hengjun Zhao; Qi Lu; ThanhVu Nguyen (Automated Reasoning and Mathematics, 2013)

Obtaining Finite Local Theory Axiomatizations via Saturation. - Matthias Horbach; Viorica Sofronie-Stokkermans (FroCos, 2013)

Locality Transfer: From Constrained Axiomatizations to Reachability Predicates. - Matthias Horbach; Viorica Sofronie-Stokkermans (IJCAR, 2014)

Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata. - Werner Damm; Matthias Horbach; Viorica Sofronie-Stokkermans (FroCos, 2015)

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

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