How to avoid the derivation of redundant clauses in reasoning systems
scientific article; zbMATH DE number 444935