摘要
This paper introduces some improvements on the intelligent backtrackingstrategy for forward chaining theorem proving. How to decide a minimal useful consequent atom setfor a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessarynon-Horn clause used for forward chaining will be split only once. The increase of the search spaceby invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. Inthis paper, the principle of the proposed method and its correctness are introduced. Moreover, someexamples are provided to show that the proposed approach is powerful for forward chaining theoremproving.
This paper introduces some improvements on the intelligent backtrackingstrategy for forward chaining theorem proving. How to decide a minimal useful consequent atom setfor a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessarynon-Horn clause used for forward chaining will be split only once. The increase of the search spaceby invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. Inthis paper, the principle of the proposed method and its correctness are introduced. Moreover, someexamples are provided to show that the proposed approach is powerful for forward chaining theoremproving.
基金
日本学术振兴会资助项目
