A proof of completeness for depth-first non-horn magic set

Miyuki Koshimura, Ryuzo Hasegawa

Research output: Contribution to journalArticlepeer-review


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 languageEnglish
Pages (from-to)111-118
Number of pages8
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Issue number2
Publication statusPublished - Sept 2002

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering


Dive into the research topics of 'A proof of completeness for depth-first non-horn magic set'. Together they form a unique fingerprint.

Cite this