The non-Horn magic sets (NHM) have been presented in order to enhance forward reasoning provers by combining top-down and bottom-up provings. The NHM method is a natural extension of Horn magic sets and is applicable to non-Horn clauses. There are two types of transformations to get non-Horn magic sets from the given clause sets: depth-first NHM and breadth-first NHM. We present a proof of completeness for depth-first NHM by giving a proof-tree transformation procedure.
|Number of pages||8|
|Journal||Research Reports on Information Science and Electrical Engineering of Kyushu University|
|Publication status||Published - Sep 2002|
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Electrical and Electronic Engineering