On the relationship between non-horn magic sets and relevancy testing
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.
KeywordsHorn Clause Ground Atom Proof Tree Ground Instance Partial Interpretation
Unable to display preview. Download preview PDF.
- 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
- 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
- 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