Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing Cesare Tinelli OriginalPaper Pages: 1 - 31
Modifying LOTOS Specifications by Means of Automatable Formula-Based Integrations Antonella SantoneGigliola Vaglini OriginalPaper Pages: 33 - 58
Formalizing Strong Normalization Proofs of Explicit Substitution Calculi in ALF Fairouz KamareddineHaiyan Qiao OriginalPaper Pages: 59 - 98
Paramodulation and Knuth–Bendix Completion with Nontotal and Nonmonotonic Orderings Miquel BofillGuillem GodoyAlbert Rubio OriginalPaper Pages: 99 - 120