How to Implement Quantifiers?

Appeared in Volume 8/3, August 1995

Keywords: quantifiers.

kramer@al.esec.ch
Reto Kramer
13th April 1995

How can existential and universal quantifiers be implemented in a readeable way?

I understand that second order programming, setof/3, and things like for_all/3 in The Art of Prolog, p.303 are the key to the solution. However when I try to translate my maths, which involves the negation of existential quantifiers, I end up with pretty unreadable code!

Is there a guideline for translating statements like:

there is no X for which predicate(X) is true
there is only a single X such that predicate(X) is true
for all X predicate(X) is true

Is there any Prolog extension that makes this easy to express (I understand that Goedel provides quantifiers as built-ins).

sdecker@informatik.uni-kl.de
Stefan Decker
13th April 1995

To ensure that a Prolog database fulfils a first-order formula amounts to the problem of integrity checking in deductive databases.

There is a simple mechanism for translating a first-order formula into a normal Prolog program by Lloyd in [Lloyd84].

If you are interested in integrity checking of deductive databases, it might be useful to check my diploma thesis (written in German!) available by anonymous FTP from:
ftp://ftp.uni-kl.de/reports_uni-kl/computer_science/deductive_databases/1994/papers/Decker.dip94.ps.gz

My thesis contains an algorithm for translating first-order formulas, based on [Lloyd84], but disjunctions are handled in a better way. Of course, it is not possible to express knowledge of arbitrary first-order formulas in Prolog, because Prolog is based on Horn clauses with negation as finite failure.

[Lloyd84] J. W. Lloyd and R. W. Topor
"Making Prolog more expressive"
Logic Programming (USA), Vol. 1, No. 3
pp. 225--40, October 1984

Abstract: This paper introduces extended programs and extended goals for logic programming. A clause in an extended program can have an arbitrary first-order formula as its body. Similarly, an extended goal can have an arbitrary first-order formula as its body. The main results of the paper are the soundness of the Negation As Failure rule and SLDNF-Resolution for extended programs and goals. The increased expressibility of extended programs and goals can be easily implemented in any Prolog system which has a sound implementation of the negation as failure rule. These ideas can be used to implement first-order logic as a query language in a deductive database system. An application to integrity constraints in deductive database systems is given.

lee@munta.cs.mu.oz.au
Lee Naish
19th April 1995

NU-Prolog also supports quantifiers, implication etc (very similar to Goedel). Your second form is not supported directly and the third form will always flounder.

The translation NU-Prolog uses also differs from [Lloyd84] slightly, to reduce floundering, if I recall correctly.

millies@coli.uni-sb.de
Sebastian Millies
20th April 1995

What about the following predicates? All make use of negation as failure and do not instantiate the quantified variable. It's probably better to call it extra-logical (rather than second-order logic) programming.

exist(X, Restriction, Scope) :-
  \+ \+ (Restriction, Scope).

exist_exactly_one(X, Restriction, Scope) :-
  setof(X, (Restriction, Scope), [_]).

exist_at_least_two(X, Restriction, Scope) :-
  setof(X, (Restriction, Scope), [_,_|_]).

all(X, Restriction, Scope) :-
  \+ (Restriction, \+ Scope).

most(X, Restriction, Scope) :-
  setof(X, Restriction, All),
  setof(X, (Restriction,Scope), Most),
  length(All, N), length(Most, M), N < 2*M.

'most Ps are Qs' is formalized here as 'There are things which are Ps and more than half of those things are also Qs'. Other truth conditions have been proposed for this quantifier. In particular, you have to be careful about whether you allow empty restrictions (domains of quantification). For example, 'all Ps are Qs' is formalized to succeed if there are no things which are Ps.

You'll get into trouble when you want to quantify over infinite domains (e.g. the natural numbers).

Reto Kramer wrote:

Is there a guideline for translating statements like:
* there is no X for which predicate(X) is true

In the above terms, this corresponds to:

?- \+ exist(X, predicate(X), true).

But can be said more simply:

?- \+ predicate(X).

dogru@cs.umn.edu
Sait Dogru
17 April 1995

Here is the relevant part of a report I wrote on an implementation of essentially the same problem. There are three steps involved. The input can be in the standard format: a variable to quantify over, a set of predicates that the variable must satisfy, and a quantifier. Valid quantifiers include the usual (universal, existential), fuzzy (most, many) and generalized ones (2 to 5, at least 10, etc.).

1) Collect Predicates

We first collect all the predicates the quantified concept participates in.

2) Find All Candidates

We next find all the instances of the quantified concept satisfying the predicate list found in the first step above. We essentially use a construct similar to bagof/3 and setof/3 predicates of logic programming languages called quantify. Quantify returns as its result a set whose elements are exactly those values of the quantified concept that satisfy the predicate list. Note that no judgment is made at this point about the result of quantify.

3) Verify Results

We finally verify that the number of elements in the set (returned by quantify) is congruent with the quantifier specified for the concept. If no quantifier is specified, the default quantifier is assumed to be 1 to infinity. (The universal quantifier is a bit more complicated as it requires an additional step that is very similar to step (2) above.

Reto Kramer wrote:

Is there a guideline for translating statements like:
* there is no X for which predicate(X) is true

This, for example, would correspond to:

?- Predicate = (predicate(X),...),  % the predicates
   quantify(X, Predicate, Result),  % basically a setof/bagof
   checkSetSize(Result, 0, 0).      % Result has min & max elements

tcmb0081@cdc8g5.cdc.polimi.it
Alessio Lomuscio
20th April 1995

Reto Kramer wrote:

How can existential and universal quantifiers be implemented in a readeable way?

I've just built a theorem prover for modal logic and had to get involved with these issues. What I tried at first was representing: every x fi(x) as all(X,fi(X))

This is a nice method, but contains problems such as troubles with the occurs check. I resolved a lot of them, but eventually I changed to: all(x,fi(x)) and ex(x,fi(x)).

You have to write more code but the situation is under more control.