Skip to main content
SpringerLink
Log in

Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

  • Conference paper
  • First Online:
Book cover Automated Deduction—CADE-14 (CADE 1997)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1249))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Akahani, J., Inoue, K. and Hasegawa, R.: Bottom-up modal theorem proving based on modal clause transformation, Trans. Information Processing Society of Japan, Vol. 36, No. 4, pp. 822–831 (1995), in Japanese.

    Google Scholar 

  2. Arayama, M. and Inoue, K.: Optimizations of query processing for disjunctive deductive databases, Trans. Information Processing Society of Japan, Vol. 37, No. 12, pp. 2295–2304 (1996), in Japanese.

    Google Scholar 

  3. Bancilhon, F., Maier, D., Sagiv, Y. and Ullman, J.D.: Magic sets and other strange ways to implement logic programs, Proc. 5th ACM SIGMOD-SIGACT Symp. on Principles of Database Systems, pp. 1–15 (1986).

    Google Scholar 

  4. Beeri, C. and Ramakrishnan, R.: On the power of magic, Proc. Sixth ACM Symp. on Principles of Database Systems, pp. 269–283 (1987).

    Google Scholar 

  5. Bry, F.: Query evaluation in recursive databases: bottom-up and top-down reconciled, Data & Knowledge Engineering, Vol. 5, pp. 289–312 (1990).

    Article  Google Scholar 

  6. Bry, F. and Yahya, A.: Minimal model generation with positive unit hyper-resolution tableaux, Proc. TABLEAUX'96, LNAI 1071, pp. 143–159 (1996).

    MATH  Google Scholar 

  7. Demolombe, R.: An efficient strategy for non-Horn deductive databases, Theoretical Computer Science, Vol. 78, pp. 245–259 (1991).

    Article  MathSciNet  Google Scholar 

  8. Loveland, D.W., Reed, D.W. and Wilson, D.S.: SATCHMORE: SATCHMO with RElevancy, J. Automated Reasoning, Vol. 14, No. 2, pp. 325–351 (1995).

    Article  MathSciNet  Google Scholar 

  9. Hasegawa, R. and Fujita, H.: A model generation theorem prover in KL1 using ramified-stack algorithm, Proc. 8th ICLP, pp. 535–548 (1991).

    Google Scholar 

  10. Hasegawa, R., Ohta, Y. and Inoue, K.: Non-Horn magic sets and their relation to relevancy testing, Technical Report ICOT-TR-834, ICOT, Tokyo, (1993).

    Google Scholar 

  11. Hasegawa, R.: Parallel theorem-proving system: MGTP, Proc. FGCS'94, pp. 51–65 (1994).

    Google Scholar 

  12. Hasegawa, R. and Koshimura, M.: An AND parallelization method for MGTP and its evaluation, Proc. Int. Symp. on PASCO'94, pp. 194–203 (1994).

    Google Scholar 

  13. Hasegawa, R. and Fujita, H.: MGTP: a model generation theorem prover in the concurrent logic programming language KL1, Trans. Information Processing Society of Japan, Vol. 37, No. 1, pp. 1–12 (1996), in Japanese.

    Google Scholar 

  14. Manthey, R. and Bry, F.: SATCHMO: a theorem prover implemented in Prolog, Proc. CADE-9, LNCS 310, pp. 415–434 (1988).

    MATH  Google Scholar 

  15. Nakashima, H., Nakajima, K., Kondoh S., Takeda Y., Inamura, Y., Onishi, S. and Masuda, K.: Architecture and implementation of PIM/m, Proc. FGCS'92, pp. 425–435 (1992).

    Google Scholar 

  16. Ohta, Y., Inoue, K. and Hasegawa, R.: The equivalence between non-Horn magic sets and relevancy testing, submitted for publication (1996), in Japanese.

    Google Scholar 

  17. Rohmer, J., Lescoeur, R. and Kerisit, J.M.: The Alexander method — a technique for the processing of recursive axioms in deductive databases, New Generation Computing, Vol. 4, pp. 273–285 (1986).

    Article  Google Scholar 

  18. Stickel, M.E.: Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, J. Automated Reasoning, Vol. 13, No. 2, pp. 189–210 (1994).

    Article  MathSciNet  Google Scholar 

  19. Suttner, C. and Sutcliffe, G.: The TPTP problem library, Technical report AR-94-03, Institut für Informatik, Technische Universität München, Munich, Germany (also available as Technical report 93/11, Department of Computer Science, James Cook University, Townsville, Australia) (1994).

    Google Scholar 

  20. Ueda, K. and Chikayama, T.: Design of the kernel language for the parallel inference machine, Computer J., Vol. 33, No. 6, pp. 494–500 (1990).

    Article  MathSciNet  Google Scholar 

  21. Yahya, A.H.: A goal-driven approach to efficient query processing in disjunctive databases, Research Report PMS-FB-1996-12, Institut für Informatik, Ludwig Maximilians Universität München (1996).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Kyushu University, Kasuga Kouen 6-1, Kasuga-shi, 816, Fukuoka, Japan

    Ryuzo Hasegawa & Miyuki Koshimura

  2. Toyohashi University of Technology, Tempaku-cho, Toyohashi-shi, 441, Aichi, Japan

    Katsumi Inoue

  3. University of Industrial Technology, Hashimotodai 4-1-1, Sagamihara-shi, 229-11, Kanagawa, Japan

    Yoshihiko Ohta

Authors
  1. Ryuzo Hasegawa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Katsumi Inoue
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yoshihiko Ohta
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Miyuki Koshimura
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

William McCune

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hasegawa, R., Inoue, K., Ohta, Y., Koshimura, M. (1997). Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-63104-6_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63104-0

  • Online ISBN: 978-3-540-69140-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation