Non-resolution theorem proving

摘要

This talk reviews those efforts in automatic theorem proving, during the past few years, which have emphasized techniques other than resolution. These include: knowledge bases, natural deduction, reduction, (rewrite rules), typing, procedures, advice, controlled forward chaining, algebraic simplification, built-in associativity and commutativity, models, analogy, and man-machine systems. Examples are given and suggestions are made for future work.