Higher-order logic in KIF and CGs

sowa <sowa@turing.pacss.binghamton.edu>

Mail folder: Interlingua Mail
Next message: olsen@cs.stanford.edu: "C++ KIF Parser"
Previous message: Tom Gruber: "high order relations in first order KIF"

Date: Tue, 23 Nov 93 18:33:32 EST
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9311232333.AA11239@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU
Subject: Higher-order logic in KIF and CGs

I would like to endorse Tom Gruber's comments about the use of
KIF for expressing Fritz Lehmann's examples.  Except for syntax and
the assumed set of primitives, that is the same kind of thing that
I have been advocating with CGs.
 
In a previous note, I mentioned the book about HOL, which is explicitly
called "Higher Order Logic", but which appears to do the same kinds
of things that we are advocating with KIF and CGs.  I don't see any
point in further vague arguments about the virtues of "true" HOL.
  
If Fritz or anyone else has a serious problem that can't be represented
in KIF and/or CGs, then we would definitely like to see a clear statement
of what it is, preferably formalized in some kind of logic (higher-order
or whatever).  The HOL book I cited earlier has many good examples;
it is an excellent place to start looking for counterexamples to our
claims that the KIF and CG semantics is sufficient.  Until we get some
specific counterexamples, there is no point in continuing this discussion.
 
John Sowa