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

Authors: 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}
  }