前件推导及其计算机实现

Antecedent Derivation and Its Implementation

前件推导是定理证明的一种扩展.本文介绍了前件推导的定义及其形式系统,描述了前件推导的计算机实现,该实现具有如下一些特点:1)主要采用自然演绎途径;2)用一种扩展与/或树表示前件推导问题;3)基本搜索策略是有序深度优先;4)利用启发信息控制搜索.

Antecedent derivation is an extension of theorem proving.This paper introduces a definition and a formal system of antecedent derivation,describes its computer implementation which has the following characteristics: ·Mainly taking the natural deduction approach. ·Using an extended AND/OR tree to represent antecedent derivation problem. ·The basic search strategy is depth first search. ·Using some heuristics to guide the search.