# Quantifier syntax in KIF

macgregor@isi.edu
Message-id: <199304081645.AA10329@quark.isi.edu>
Reply-To: cg@cs.umn.edu
Date: Thu, 8 Apr 1993 09:44:50 -0800
To: sowa <sowa@turing.pacss.binghamton.edu>, cg@cs.umn.edu,
interlingua@ISI.EDU, srkb@ISI.EDU
From: macgregor@isi.edu
Subject: Quantifier syntax in KIF

John Sowa's recent suggestion to add some sugar-coating to KIF
brings up the question of what a syntax for typed quantifiers
or scoped quantifiers should look like.
In the current KIF, multiple quantified variables can be written as:
(exists (?x ?y) ...)
A single *typed* variable might be written either as
(exists (?x Block) ...)
or
(exists ((?x Block)) ...)
I would recommend the latter syntax. Otherwise, the meaning of the
quantifier construct varies depending on whether a term is a variable or a
constant. Similarly, if we consider adding "in", I would favor the syntax
(exists ((?s set))
(forall ((?x in ?s)) ...))
rather than
(exists ((?s set))
(forall (?x in ?s) ...))
Thus, the following example in John's last message:
> (exists (set ?s)
> (and (count ?s 3)
> (forall (?p in ?s)
> (and (pyramid ?p)
> (unique (?b block) (on ?p ?b)) ))))
>
would be rephrased as
(exists ((?s set))
(and (count ?s 3)
(forall ((?p in ?s))
(and (pyramid ?p)
(unique ((?b block)) (on ?p ?b)) ))))
- Bob
Robert M. MacGregor macgregor@isi.edu
USC/ISI, 4676 Admiralty Way, Marina del Rey, CA 90292 (310) 822-1511