Some methods to decrease the number of clauses obtained by Non-Horn magic sets transformation and their evaluation

Miyuki Koshimura, Ryuzo Hasegawa, Tomohiro Tanaka

Research output: Contribution to journalArticle

Abstract

Non-Horn magic sets(NHM) method transforms a given clause set into a set of clauses simulating backward reasoning and those for controlling forward reasoning so as to prune the search space. To preserve the range-restricted condition, the transformation needs to attach an adornment to a predicate to show binding information of its arguments. However, introducing adornments causes combinatorial explosion of the number of transformed clauses because the number of adornments may increase exponentially. This paper presents four methods to decrease the number of transformed clauses: (1) obtaining necessary adornments by statical analysis, (2) extracting minimal adornments from necessary adornments, (3) calculating necessary adornments dynamically, and (4) transformation without adornments. These methods have been implemented on a UNIX workstation. We evaluated their effects by proving some problems in the TPTP problem library.

Original languageEnglish
Pages (from-to)247-252
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Volume2
Issue number2
Publication statusPublished - Sep 1 1997

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Some methods to decrease the number of clauses obtained by Non-Horn magic sets transformation and their evaluation'. Together they form a unique fingerprint.

  • Cite this