Skip to main content
SpringerLink
Log in

Representing infinite sequences of resolvents in recursive First-Order Horn Databases

  • Conference paper
  • First Online:
Book cover 6th Conference on Automated Deduction (CADE 1982)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 138))

Included in the following conference series:

Abstract

A First Order Database is defined as a function-free First-Order Theory in which the ground units serve as the Extensional Database and the proper non-logical axioms serve as the Intensional Database. This paper addresses the following problem: “Given a recursive non-logical axiom and a theorem to be proved which interacts with this axiom, can we describe a set of finite retrieval requests such that all and only the correct proofs to the theorem are found”. Our solution uses resolution-proof techniques over connection graphs to derive a program of retrieval requests from the Extensional Database that gives all the answers to a query and has a well-defined termination condition.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Aho and J. Ullman, “The Theory of Parsing, Translation, and Compiling, Vol. 1: Parsing,” Prentice-Hall, Englewood Cliffs, N.J., 1972.

    Google Scholar 

  2. C. Chang, “On Evaluation of Queries Containing Derived Relations in a Relational Data Base,” Workshop on Formal Basis for Databases, Toulouse, France, 1979.

    Google Scholar 

  3. L. Henshen, S. Naqvi, “On Compiling Queries in Recursive First-Order Databases”, submitted to JACM.

    Google Scholar 

  4. R. Reiter, “Deductive Question Answering on Relational Data Bases,” in Logic and Data Bases (ed. H. Gallaire and J. Minker), Plenum Press, 1978.

    Google Scholar 

  5. R. Reiter, “Equality and Domain Closure for First-Order Data Bases,” Journal of the ACM, Vol. 27, No. 2, 1980.

    Google Scholar 

  6. J. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle,” Journal of the ACM, Vol. 12, No. 1, 1965.

    Google Scholar 

  7. S. Shapiro, and D. McKay, “Inference with Recursive Rules,” Proc. NCAI, Stanford University, 1980.

    Google Scholar 

  8. S. Sickel, “A Search Technique for Clause Interconnectivity Graphs,” IEEE transactions on computers, Vol. C-25, No. 8, 1976.

    Google Scholar 

  9. J. Ullman, “Principles of Data Base Systems,” Computer Science Press, Potomac, Md., 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Northwestern University, 60201, Evanston, Illinois

    Lawrence J. Henschen

  2. Bell Laboratories, 07974, Murray Hill, New Jersey

    Shamim A. Naqvi

Authors
  1. Lawrence J. Henschen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shamim A. Naqvi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

D. W. Loveland

Rights and permissions

Reprints and permissions

Copyright information

© 1982 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Henschen, L.J., Naqvi, S.A. (1982). Representing infinite sequences of resolvents in recursive First-Order Horn Databases. In: Loveland, D.W. (eds) 6th Conference on Automated Deduction. CADE 1982. Lecture Notes in Computer Science, vol 138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000069

Download citation

  • DOI: https://doi.org/10.1007/BFb0000069

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-11558-8

  • Online ISBN: 978-3-540-39240-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation