Homepage

Matthias Horbach

Matthias Horbach

Group of Deepak Kapur
Department of Computer Science
Farris Engineering Center
MSC 01 1130
University of New Mexico
Albuquerque, NM 87131
United States of America

Email: horbach@cs.unm.edu
Phone: +1 505 277-0799
Fax: +1 505 277-6927

Research Interests

  • Automated and Inductive Theorem Proving
  • Program Analysis
  • Proof Nets
  • Algebraic Geometry

Publications

My publications at dblp

If you have questions about submitted papers but prefer to remain anonymous (e.g. because you are a referee), please contact me via the contact form!

Journal Articles

  • Horbach, M. and Weidenbach, C., 2010, Superposition for Fixed Domains
    In ACM Transactions on Computational Logics 11(4).

Conference Articles

  • Horbach, M., 2011, Predicate Completion for Non-Horn Clause Sets
    In Proc. of the 23rd International Conference on Automated Deduction, CADE-23, 2011, LNAI 6803, 300-315.
    The original publication is available at www.springerlink.com.
  • Horbach, M., 2011, System Description: SPASS-FD
    In Proc. of the 23rd International Conference on Automated Deduction, CADE-23, 2011, LNAI 6803, 316-322.
    The original publication is available at www.springerlink.com.
  • Horbach, M., 2010, Disunification for Ultimately Periodic Interpretations
    In Proc. of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16, LNAI 6355, 290-311.
    The original publication is available at www.springerlink.com.
  • Horbach, M. and Weidenbach, C., 2009, Deciding the Inductive Validity of Forall Exists* Queries
    In Proc. of the 18th Annual Conference of the European Association for Computer Science Logic, CSL 2009, LNCS 5771, 332-347.
    The original publication is available at www.springerlink.com.
  • Horbach, M. and Weidenbach, C., 2009, Decidability Results for Saturation-Based Model Building
    In Proc. of the 22nd International Conference on Automated Deduction, CADE-22, 2009, LNAI 5663, 404-420.
    The original publication is available at www.springerlink.com.
  • Horbach, M. and Weidenbach, C., 2008, Superposition for Fixed Domains.
    In Proc. of the 17th Annual Conference of the European Association for Computer Science Logic, CSL 2008, LNCS 5213, 293-307.
    The original publication is available at www.springerlink.com.

Technical Reports

  • Horbach, M. and Weidenbach, C., 2009, Deciding the Inductive Validity of Forall Exists* Queries
    Technical Report MPI-I-2009-RG1-001.
  • Horbach, M. and Weidenbach, C., 2009, Decidability Results for Saturation-Based Model Building
    Technical Report MPI-I-2009-RG1-004.
  • Horbach, M. and Weidenbach, C., 2009, Superposition for Fixed Domains.
    Technical Report MPI-I-2009-RG1-005.

Theses

  • Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics
    Ph.D. thesis, Department of Computer Science, Saarland University, 2010
  • Proof Nets for Intuitionistic Logic
    Diploma thesis, Department of Computer Science, Saarland University, 2006
  • Die Transformation von Tate-Auflösungen unter Veronese-Einbettungen (The Transformation of Tate Resolutions under Veronese Embeddings)
    Diploma thesis, Department of Mathematics, Saarland University, 2005
  • Incremental Algorithms and a Minimal Graph Representation for Regular Trees
    Advanced practical, Department of Computer Science, Saarland University, 2002, joint work with Sven Woop

Software

   Please visit the software section of this homepage.

Employment