A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
scientific article; zbMATH DE number 7763325
scientific article