A relevance restriction strategy for automated deduction
scientific article; zbMATH DE number 5003861