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 language | English (US) |
|---|---|
| Title of host publication | Unknown Host Publication Title |
| Publisher | IEEE |
| Pages | 98-105 |
| Number of pages | 8 |
| ISBN (Print) | 0818607939 |
| State | Published - 1987 |