Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 111-118 |
| Number of pages | 8 |
| Journal | Research Reports on Information Science and Electrical Engineering of Kyushu University |
| Volume | 7 |
| Issue number | 2 |
| Publication status | Published - Sept 2002 |
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Electrical and Electronic Engineering