HEREDITARY HARROP FORMULAS AND UNIFORM PROOF SYSTEMS.

Dale Miller, Gopalan Nadathur, Andre Scedrov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Scopus citations

Abstract

The authors are concerned with strengthening the logical foundations of the logic programming paradigm. In particular, they 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 are called uniform proof systems. For the purposes of this paper, a logic programming language is identified with any logical system whose proof predicate is uniform. They present three logic programming languages which extend the positive Hern clause logic programming language. The most expressive language is based on hereditary Harrop formulas and uses higher-order intuitionistic logic as its proof system. Several metatheoretic properties of hereditary Harrop formulas are presented.

Original languageEnglish (US)
Title of host publicationUnknown Host Publication Title
PublisherIEEE
Pages98-105
Number of pages8
ISBN (Print)0818607939
StatePublished - Jan 1 1987

Fingerprint Dive into the research topics of 'HEREDITARY HARROP FORMULAS AND UNIFORM PROOF SYSTEMS.'. Together they form a unique fingerprint.

  • Cite this

    Miller, D., Nadathur, G., & Scedrov, A. (1987). HEREDITARY HARROP FORMULAS AND UNIFORM PROOF SYSTEMS. In Unknown Host Publication Title (pp. 98-105). IEEE.