Logic Programming with Bounded Quantifiers

EasyChair Preprint 3169

Abstract

This is a copy of technical report ECRC 1992-92-29 published by the author in October 1992. ECRC technical reports are no more accessible and I could not find any trace of ECRC, so I decided to publish it as a preprint. The paper was submitted to the Journal of Logic Programming, then I was asked to revise it, and then the journal ceased to exist because of a disagreement between the research community and Elsevier Science. Then my interest shifted from logic programming to theorem proving and I could never find time to publish this material.

Original Abstract:

This paper describes an extension of Horn clause logic programs by bounded quantifiers. Bounded quantifiers had been extensively used in a part of mathematical logic called the theory of admissible sets [Barwise 1975]. Later some variants of bounded quantifiers had been introduced in logic programming languages [Goncharov 1985, Schwartz 1986, Turner 1986, Kuper 1987, Dovier 1991,Hentenryck 1991]. We show that an extension of logic programs by bounded quantifiers has several equivalent logical semantics and is efficiently implementable using a variant of SLD-resolution, which we call SLDB-resolution.  We give examples showing that introduction of bounded quantifiers results in a high level logical specification language. The expressive power of subsets of Horn clauses and subsets of logic programs with bounded quantifiers is compared. We also show that the use of bounded quantifiers sheds new light on classical negation in logic programming.

Keyphrases: bounded quantifiers, computability, hereditarily finite sets, logic programming

@booklet{EasyChair:3169,
  author    = {Andrei Voronkov},
  title     = {Logic Programming with Bounded Quantifiers},
  howpublished = {EasyChair Preprint 3169},
  year      = {EasyChair, 2020}}