Quantifier syntax in KIF

• Mail folder: SRKB Mail
• Next message: phayes@cs.uiuc.edu: "Re: Issues about contexts and quantifiers"
• Previous message: sowa: "Interoperability of O-O languages and databases"
• Reply: Michael R. Genesereth: "Re: 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) ...)
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