Extensions of the Knuth-Bendix Ordering with LPO-like Properties,
with Michel Ludwig.
Submitted, February 2007.
Automated Web service discovery using theorem provers,
with Ruzica Piskac et al.
Submitted, December 2006.
Combining SAT, AIGs and first-order reasoning in the verification of hybrid systems,
with Werner Damm et al.
Submitted, December 2006.
Automatic verification of hybrid systems with large discrete state space,
with Werner Damm et al.
In ATVA 2006, pp. 276-291, 2006.
Modular proof systems for partial functions with Evans equality,
with Harald Ganzinger and Viorica Sofronie-Stokkermans.
In I&C, 204:1453-1492, 2006.
SPASS+T,
with Virgile Prevosto.
In ESCoR, pp. 18-33, 2006.
Comparing instance generation methods for automated reasoning,
with Swen Jacobs.
In TABLEAUX 2005, LNAI 3702, pp. 153-168, 2005.
Revised version accepted for JAR.
Modular proof systems for partial functions with weak equality,
with Harald Ganzinger and Viorica Sofronie-Stokkermans.
In IJCAR 2004, LNAI 3097, pp. 168-182, 2004.
Superposition modulo a Shostak theory,
with Harald Ganzinger and Thomas Hillenbrand.
In CADE-19, LNAI 2741, pp. 182-196, 2003.
Cancellative abelian monoids and related structures in refutational theorem proving (Part I).
In JSC, 33(6):777-829, 2002.
Cancellative abelian monoids and related structures in refutational theorem proving (Part II).
In JSC, 33(6):831-861, 2002.
A new input technique for accented letters in alphabetical scripts.
In IUC 20, 2002.
Superposition and chaining for totally ordered divisible abelian groups.
In IJCAR 2001, LNAI 2083, pp. 226-241, 2001.
Cancellative superposition decides the theory of divisible torsion-free abelian groups.
In LPAR'99, LNAI 1705, pp. 131-147, 1999.
Extending reduction orderings to ACU-compatible reduction orderings.
In IPL, 67(1):43-49, 1998.
Superposition for divisible torsion-free abelian groups.
In CADE-15, LNAI 1421, pp. 144-159, 1998.
Cancellative Abelian Monoids in Refutational Theorem Proving.
PhD Thesis, Universität des Saarlandes, 1997.
Theorem proving in cancellative abelian monoids,
with Harald Ganzinger.
In CADE-13, LNAI 1104, pp. 388-402, 1996.
Refutational theorem proving for hierarchic first-order theories,
with Leo Bachmair and Harald Ganzinger.
In AAECC, 5(3/4):193-212, 1994.
Superposition with simplification as a decision procedure for the monadic class with equality,
with Leo Bachmair and Harald Ganzinger.
In KGC'93, LNCS 713, pp. 83-96, 1993.
Set constraints are the monadic class,
with Leo Bachmair and Harald Ganzinger.
In LICS 8, pp. 75-83, 1993.
Theorem proving for hierarchic first-order theories,
with Leo Bachmair and Harald Ganzinger.
In ALP'92, pp. 420-434, 1992.
Termination proofs of well-moded logic programs via conditional rewrite systems,
with Harald Ganzinger.
In CTRS'92, LNCS 656, pp. 430-437, 1992.
Semantics of order-sorted specifications.
In TCS, 94(1):1-35, 1992.
Compatibility of order-sorted rewrite rules.
In CTRS'90, LNCS 516, pp. 407-416, 1990.
Unitary unification in order-sorted signatures (extended abstract).
In UNIF'89, pp. 106-110, 1989.
ESARLT, CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, July 2007 (PC member)
ESCoR, FLoC'06 Workshop on Empirically Successful Computerized Reasoning, Seattle, USA, August 2006 (PC member)
RTA'03, 14th International Conference on Rewriting Techniques and Applications, Valencia, Spain, June 9-11, 2003 (PC member)
AVACS - Automatic Verification and Analysis of Complex Systems
Verisoft - Beweisen als Ingenieurwissenschaft (until June 2006)
PhD in Computer Science (Dr.-Ing.), Universität des Saarlandes, July 1997.
Thesis:
Cancellative
Abelian Monoids in Refutational Theorem Proving.
Diploma in Computer Science (Dipl.-Inf.), Universität Dortmund, August 1989.
Thesis: Vervollständigung von Spezifikationen mit Subsortendeklarationen
(Completion of Specifications with Subsort Declarations).