@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.}",
note = "Publisher Copyright: {\textcopyright} 1982, Springer-Verlag.; 6th Conference on Automated Deduction, CADE 1982 ; Conference date: 07-06-1982 Through 09-06-1982",
year = "1982",
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",
}