Comparing Instance Generation Methods for Automated Reasoning, with Swen Jacobs.
Modular Proof Systems for Partial Functions with Weak Equality, with Harald Ganzinger and Viorica Sofronie-Stokkermans.
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.
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
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).