@inproceedings{7f0c5007d7204c4ab153f891f67f4766,
title = "Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving",
abstract = "We present a new method, called non-Horn magic sets (NHM), to enhance forward reasoning provers by combining top-down and bottom-up computations. This method is a natural extension of Horn magic sets and is applicable to range-restricted non-Horn clauses. We show two types of transformations to get non-Horn magic sets from the given clause sets: breadth-first NHM and depth-first NHM. The first transformation evaluates the antecedent atoms of an original clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent atom to the next by using continuation predicates. These transformations are shown to be sound and complete. The NHM method has been implemented on a UNIX workstation. We evaluated effects of NHM by proving some typical problems taken from the TPTP problem library.",
author = "Ryuzo Hasegawa and Katsumi Inoue and Yoshihiko Ohta and Miyuki Koshimura",
year = "1997",
doi = "10.1007/3-540-63104-6_18",
language = "English",
isbn = "3540631046",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "176--190",
editor = "William McCune",
booktitle = "Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings",
address = "Germany",
note = "14th International Conference on Automated Deduction, CADE 1997 ; Conference date: 13-07-1997 Through 17-07-1997",
}