KIF (David McAllester)
From: (David McAllester)
Date: Tue, 7 Jan 92 13:44:41 EST
Message-id: <9201071844.AA03125@raisin-bran>
Subject: KIF 

    On the contrary, there is a growing interest in higher order logic,
    or at least a carefully chosen subset of higher order logic that
    will allow us to naturally represent many of the everyday sort of
    statements (and allow reasonable inferences from them).

Sounds interesting.  Have you considered whether the subsets of
higher order logic allow truely increased expressive power?  For
example, do they allow a definition of transitive closure?  The Kl-ONE
primitives I am aware of do not really extend the expressive power
beyond that of first order logic.  Why not simply allow
arbitrary quantification over functions and predicates?