| Creator |
|
|
|
| Language |
|
| Publisher |
|
|
|
| Date |
|
| Source Title |
|
| Vol |
|
| Issue |
|
| First Page |
|
| Last Page |
|
| Publication Type |
|
| Access Rights |
|
| JaLC DOI |
|
| Related DOI |
|
| Related URI |
|
| Relation |
|
| 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 a...nd 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.show more
|
Export Mendeley
p111