Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing
Modifying LOTOS Specifications by Means of Automatable Formula-Based Integrations
Formalizing Strong Normalization Proofs of Explicit Substitution Calculi in ALF
Paramodulation and Knuth–Bendix Completion with Nontotal and Nonmonotonic Orderings*