## Paper: Hereditary Harrop Formulas and Uniform Proof Systems (at LICS 1987)

**Dale A. Miller Gopalan Nadathur Andre Scedrov**

### Abstract

In this paper, we are concerned with strenthening the logical
foundations of the logic programming paradigm. In particular, we are interested
in those logical systems whose provability predicate preserves a simple and
natural search-related interpretation of the logical connectives. Proof systems
which are sound and complete for this interpretation will be called *uniform
proof systems*. For the purposes of this paper, we will identify a logic
programming language with any logical system whose proof predicate is
uniform. We present three logic programming languages which extend the positve
Horn clause logic programming language. Our most expressive language is based
on *hereditary Harrop formulas* and uses higher-order intuitionistic
logic as its proof system. We also present several metatheoretic properties of
hereditary Harrop formulas.

### BibTeX

@InProceedings{MillerNadathurScedr-HereditaryHarropFor, author = {Dale A. Miller and Gopalan Nadathur and Andre Scedrov}, title = {Hereditary Harrop Formulas and Uniform Proof Systems}, booktitle = {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)}, year = {1987}, month = {June}, pages = {98--105}, location = {Ithaca, NY, USA}, publisher = {IEEE Computer Society Press} }