机器定理证明中的一般问题

木文从人工智能角度阐述了机器定理证明的重要意义,综述了以逻辑方法为重点的定理证明器的一般问题,如搜索策略、化简、语义、抽象、发现相关公理以及它涉及的一般软件工程问题。