Extensions to logic programming motivated by the construction of a generic theorem prover

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

Abstract

In this article, we discuss several possible extensions to traditional logic programming languages. The specific extensions proposed here fall into two categories: logical extensions and the addition of constructs to allow for increased control. There is a unifying theme to the proposed logical extensions, and that is the scoped introduction of extensions to a programming context. More specifically, these extensions are the ability to introduce variables whose scope is limited to the term in which they occur (i.e. λ-bound variables within A-terms), the ability to introduce into a goal a fresh constant whose scope is limited to the derivation of that goal, and the ability to introduce into a goal a program clause whose scope is limited to the derivation of that goal. The purpose of the additions for increased control is to facilitate the raising and handling of failures. To motivate these various extensions, we have repeatedly appealed to examples related to the construction of a generic theorem prover. It is our thesis that this problem domain is specific enough to lend focus when one is considering various language constructs, and yet complex enough to encompass many of the general difficulties found in other areas of symbolic computation.

Original languageEnglish (US)
Title of host publicationExtensions of Logic Programming - International Workshop, Proceedings
EditorsPeter Schroeder-Heister
PublisherSpringer-Verlag
Pages223-244
Number of pages22
ISBN (Print)9783540535904
DOIs
StatePublished - Jan 1 1991
Externally publishedYes
EventInternational Workshop on Extensions of Logic Programming, 1989 - Tubingen, Germany
Duration: Dec 8 1989Dec 10 1989

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume475 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherInternational Workshop on Extensions of Logic Programming, 1989
CountryGermany
CityTubingen
Period12/8/8912/10/89

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Gunter, E. L. (1991). Extensions to logic programming motivated by the construction of a generic theorem prover. In P. Schroeder-Heister (Ed.), Extensions of Logic Programming - International Workshop, Proceedings (pp. 223-244). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 475 LNAI). Springer-Verlag. https://doi.org/10.1007/BFb0038696