Implementation techniques for scoping constructs in logic programming

Bharat Jayaraman, Gopalan Nadathur

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

11 Scopus citations


Introducing universal quantifiers and some forms of implications into goals provides for scoping constructs in logic programming. We address the new implementation problems raised by the addition of these logical symbols. The presence of mixed sequences universal and existential quantifiers in goals requires unification to respect this ordering, a problem we solve by using a scheme for tagging constants and variables. A few changes to existing WAM (Warren Abstract Machine) instructions suffice to implement this scheme. Implication in goals cause new program clauses to be introduced, and the implementation must therefore accommodate a dynamically changing set of program clauses. A naive asserting and retracting of program clauses is an unsatisfactory solution to this problem in view of backtracking. Further, when an implication goal is surrounded by existential quantifiers, the introduced program clauses may have to be parameterized by the bindings for these existential variables, thus requiring program clauses to be treated as program closures. We use a hash-table for efficient access to the clauses and a new kind of record, called an implication point record, to manage the interaction between backtracking and dynamic nesting of implication goals. New instructions for the WAM are proposed for compiling quantifiers and implications in goals.

Original languageEnglish (US)
Title of host publicationLogic Program Proc 8 Int Conf
PublisherPubl by MIT Press
Number of pages16
StatePublished - Dec 1 1991
EventLogic Programming - Proceedings of the 8th International Conference - Paris, Fr
Duration: Jun 24 1991Jun 28 1991


OtherLogic Programming - Proceedings of the 8th International Conference
CityParis, Fr


Dive into the research topics of 'Implementation techniques for scoping constructs in logic programming'. Together they form a unique fingerprint.

Cite this