Quantifier syntax in KIF

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) ...)
   (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