Antecedent Derivation and Its Implementation

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.