@inproceedings{400000537a5e4c4fbe259859d9b5806f,

title = "Representing infinite sequences of resolvents in recursive First-Order horn databases",

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.",

author = "Henschen, {Lawrence J.} and Naqvi, {Shamim A.}",

year = "1982",

month = jan,

day = "1",

doi = "10.1007/BFb0000069",

language = "English (US)",

isbn = "9783540115588",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "342--359",

editor = "D.W. Loveland",

booktitle = "6th Conference on Automated Deduction",

address = "Germany",

note = "6th Conference on Automated Deduction, CADE 1982 ; Conference date: 07-06-1982 Through 09-06-1982",

}