On compiling queries in recursive first-order databases
Lawrence J. Henschen, Shamim A. Naqvi · Journal of the ACM · 1984
A first-order database ~s defined as a function-free first-order theory in which the ground units serve as the extensional database and the proper noniogical axioms serve as the intensional database.The following problem is addressed: "Given a recurswe nonlogical axiom and the form of a potential query, can one describe a set of database retrieval requests that gives the correct answers and is guaranteed to terminate."The solution uses resolution-proof techmques over connection graphs to derive a program of relational database operations that gives all the answers to a query and has a welldefined termmatton condiUon.