|
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
The documents distributed by this page have been provided by the
contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and
all rights therein are maintained by the authors or by other copyright
holders, notwithstanding that they have offered their works here
electronically. It is understood that all persons copying this information
will adhere to the terms and constraints invoked by each author's copyright.
These works may not be reposted without the explicit permission of the
copyright holder. Articles published in the
LNCS / LNAI
series © Springer-Verlag.
This web page is maintained by Thomas Hillenbrand <hillen@mpi-sb.mpg.de>. Imprint / Impressum | Data Protection / Datenschutzhinweis
Document last modified on Thursday, 24-May-2018 20:33:28 CEST.