On the relationship between non-horn magic sets and relevancy testing

  • Yoshihiko Ohta
  • Katsumi Inoue
  • Ryuzo Hasegawa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


Model-generation based theorem provers such as SATCHMO and MGTP suffer from a combinatorial explosion of the search space caused by clauses irrelevant to the goal (negative clause) to be solved. To avoid this, two typical methods have been proposed. One is relevancy testing implemented in SATCHMORE by Loveland et al., and the other is non-Horn magic sets that are the extension of Horn magic sets and used for MGTP. In this paper, we define the concept of weak relevancy testing, which somewhat relaxes the relevancy testing constraint. Then, we analyze the relationship between non-Horn magic sets and weak relevancy testing in detail, and prove that the total number of interpretations generated by MGTP employing non-Horn magic sets is always the same as that by SATCHMORE using weak relevancy testing. Thus, we find that non-Horn magic sets and weak relevancy testing, although they are completely different approaches, have the same power in pruning redundant branches of a proof tree.


Horn Clause Ground Atom Proof Tree Ground Instance Partial Interpretation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bancilhon, F., Maier, D., Sagiv, Y., and Ullman, J. D., Magic sets and other strange ways to implement logic programs, in: Proc. 5th ACM SIGMOD-SIGACT Symp. on Principles of Database Systems, pp. 1–15, 1986.Google Scholar
  2. 2.
    Beeri, C. and Ramakrishnan, R., On the power of magic, J. Logic Programming, 10:255–299, 1991.CrossRefMathSciNetGoogle Scholar
  3. 3.
    Fujita, H. and Hasegawa, R., A model generation theorem prover in KL1 using a ramified-stack algorithm, Proc. 8th Int. Conf. on Logic Programming, pp. 535–548, MIT Press, 1991.Google Scholar
  4. 4.
    Hasegawa, R., Inoue, K., Ohta, Y. and Koshimura, M., Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving, in: W. McCune (ed.), Proc. 14th Int. Conf. on Automated Deduction (CADE-14), Lecture Notes in Artificial Intelligence, 1249, pp. 176–190, Springer, 1997.Google Scholar
  5. 5.
    Lloyd, J. W., Foundations of Logic Programming, 2nd Edition, Springer, 1987.Google Scholar
  6. 6.
    Loveland, D.W., Reed, D. and Wilson, D.S., SATCHMORE: SATCHMO with RElevancy, J. Automated Reasoning, 14(2):325–351, 1995.CrossRefMathSciNetGoogle Scholar
  7. 7.
    Manthey, R. and Bry, F., SATCHMO: a theorem prover implemented in Prolog, in: E. Lusk and R. Overbeek (eds.), Proc. 9th Int. Conf. on Automated Deduction (CADE-9), Lecture Notes in Computer Science, 310, pp. 415–434, Springer, 1988.Google Scholar
  8. 8.
    Seki, H., On the power of Alexander templates, Proc. 8th ACM SIGACT-SIGMOD-SIGART Symp. on Principles of Database Systems, pp. 150–158, 1989.Google Scholar
  9. 9.
    Stickel, M. E., Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, J. Automated Reasoning, 13(2):189–210, 1994.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Yoshihiko Ohta
    • 1
  • Katsumi Inoue
    • 2
  • Ryuzo Hasegawa
    • 3
  1. 1.Department of Information EngineeringUniversity of Industrial TechnologyKanagawaJapan
  2. 2.Department of Electrical and Electronics EngineeringKobe UniversityKobeJapan
  3. 3.Department of Intelligent SystemsKyushu UniversityFukuokaJapan

Personalised recommendations