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

## Abstract

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.

## Keywords

Horn Clause Ground Atom Proof Tree Ground Instance Partial Interpretation## Preview

Unable to display preview. Download preview PDF.

## References

- 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.Beeri, C. and Ramakrishnan, R., On the power of magic,
*J. Logic Programming*, 10:255–299, 1991.CrossRefMathSciNetGoogle Scholar - 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.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.Lloyd, J. W.,
*Foundations of Logic Programming*, 2nd Edition, Springer, 1987.Google Scholar - 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.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.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.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