Thomas Hillenbrand

Research Interests

• Advancement and Application of Theorem Proving Systems
  
  
• Combination of Decision Procedures and First-order Calculi

Publications

• Th. Hillenbrand. Superposition and Decision Procedures - Back and Forth. Dissertation, Universität des Saarlandes, 2008. BibTeX
  
  
• Th. Hillenbrand and Chr. Weidenbach. Superposition for Finite Domains. Research Report MPI-I-2007-RG1-002, Max-Planck-Institut für Informatik Saarbrücken, 2007. BibTeX
  
  
• Chr. Weidenbach, R. Schmidt, Th. Hillenbrand, R. Rusev and D. Topic. SPASS version 3.0. In F. Pfenning, editor, Proceedings of the 21st International Conference on Automated Deduction, volume 4603 of LNAI, pages 514-520. Springer-Verlag, 2007. BibTeX
  
  
• Th. Hillenbrand, D. Topic, and Chr. Weidenbach. Sudokus as logical puzzles. In W. Ahrendt, P. Baumgartner, and H. de Nivelle, editors, Proceedings of the Third Workshop on Disproving, pages 2-12, 2006. BibTeX
  
  
• Th. Hillenbrand. A superposition view on Nelson-Oppen. In U. Sattler, editor, Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning, volume 106 of CEUR Workshop Proceedings, pages 16-20, 2004. BibTeX
  
  
• H. Ganzinger, Th. Hillenbrand, and U. Waldmann. Superposition modulo a Shostak theory. In F. Baader, editor, Proceedings of the 19th International Conference on Automated Deduction, volume 2741 of LNAI, pages 182-196. Springer-Verlag, 2003. BibTeX
  
  
• J.-M. Gaillourdet, Th. Hillenbrand, B. Löchner, and H. Spies. The new WALDMEISTER loop at work. In F. Baader, editor, Proceedings of the 19th International Conference on Automated Deduction, volume 2741 of LNAI, pages 317-321. Springer-Verlag, 2003. BibTeX
  
  
• Th. Hillenbrand. CITIUS ALTIUS FORTIUS: Lessons learned from the theorem prover WALDMEISTER (invited paper). In I. Dahn and L. Vigneron, editors, Proceedings of the 4th International Workshop on First-Order Theorem Proving, volume 86.1 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2003. Slides BibTeX
  
  
• J. Avenhaus, Th. Hillenbrand, and B. Löchner. On using ground joinable equations in equational theorem proving. Journal of Symbolic Computation, 36(1-2):217-233,2003. BibTeX
  
  
• B. Löchner and Th. Hillenbrand. A phytography of WALDMEISTER. AI Communications, 15(2-3):127-133, 2002. BibTeX
  
  
• Chr. Weidenbach, U. Brahm, Th. Hillenbrand, E. Keen, Chr. Theobald, and D. Topic. SPASS version 2.0. In A. Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction, volume 2392 of LNAI, pages 275-279. Springer-Verlag, 2002. BibTeX
  
  
• Th. Hillenbrand and B. Löchner. The next WALDMEISTER loop. In A. Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction, volume 2392 of LNAI, pages 486-500. Springer-Verlag, 2002. BibTeX
  
  
• Th. Hillenbrand, A. Podelski, and D. Topic. Is logic effective for analyzing C programs? In W. Charatonik and H. Ganzinger, editors, Proceedings of the Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, Research Report MPI-I-2002-2-007, pages 27-30. Max-Planck-Institut für Informatik Saarbrücken, 2002. BibTeX
  
  
• Th. Hillenbrand and B. Löchner. The next WALDMEISTER loop (extended abstract). In H. de Nivelle and S. Schulz, editors, Proceedings of the Second International Workshop on the Implementation of Logics, Research Report MPI-I-2001-2-006, pages 13-21. Max-Planck-Institut für Informatik Saarbrücken, 2001. BibTeX
  
  
• B. Afshordel, Th. Hillenbrand, and Chr. Weidenbach. First-order atom definitions extended. In R. Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 2250 of LNAI, pages 309-319. Springer-Verlag, 2001. BibTeX
  
  
• R. Nieuwenhuis, Th. Hillenbrand, A. Riazanov, and A. Voronkov. On the evaluation of indexing techniques for theorem proving. In R. Goré, A. Leitsch, and T. Nipkow, editors, Proceedings of the First International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pages 257-271. Springer-Verlag, 2001. BibTeX
  
  
• J. Avenhaus, Th. Hillenbrand, and B. Löchner. On using ground joinable equations in equational theorem proving. In P. Baumgartner and H. Zhang, editors, Proceedings of the Third International Workshop on First-Order Theorem Proving, Fachberichte Informatik 5/2000, pages 33-43. Universität Koblenz-Landau, 2000. BibTeX
  
  
• Th. Hillenbrand and B. Löchner. Shorter fixed point combinators with WALDMEISTER and the kernel strategy. Association for Automated Reasoning Newsletter, 46, 2000. BibTeX
  
  
• Th. Hillenbrand. Schnelles Gleichheitsbeweisen: Vom Vervollständigungskalkül zum WALDMEISTER-System. Diplomarbeit, Universität Kaiserslautern, Fachbereich Informatik, 2000. BibTeX
  
  
• Th. Hillenbrand, A. Jaeger, and B. Löchner. System description: WALDMEISTER - improvements in performance and ease of use. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction, volume 1632 of LNAI, pages 232-236. Springer-Verlag, 1999. BibTeX
  
  
• Th. Deiß and Th. Hillenbrand. A case study on the use of SDL. SFB 501 Internal Report 03/97, Universität Kaiserlautern, 1997. BibTeX
  
  
• Th. Hillenbrand, A. Buch, R. Vogt, and B. Löchner. WALDMEISTER: High performance equational deduction. Journal of Automated Reasoning, 18(2):265-270, 1997. BibTeX
  
  
• A. Buch and Th. Hillenbrand. WALDMEISTER: Development of a high performance completion-based theorem prover. SEKI Report 96-01, Universität Kaiserslautern, 1996. BibTeX
  
  
• A. Buch, Th. Hillenbrand, and R. Fettig. WALDMEISTER: High performance equational theorem proving. In J. Calmet and C. Limongelli, editors, Proceedings of the 4th International Symposium on Design and Implementation of Symbolic Computation Systems, volume 1128 of LNCS, pages 63-64, 1996. BibTeX
  
  
• Th. Hillenbrand, A. Buch, and R. Fettig. On gaining efficiency in completion-based theorem proving. In H. Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1103 of LNCS, pages 432-435. Springer-Verlag, 1996. BibTeX

Copyright