Higher-Order Logic

sowa <sowa@turing.pacss.binghamton.edu>
Reply-To: cg@cs.umn.edu
Date: Wed, 10 Nov 93 17:58:33 EST
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9311102258.AA15237@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@isi.edu
Subject: Higher-Order Logic

Fritz, Pat, Dan, Tomas, and anyone else who may be interested in HOL,

I endorse Tomas Uribe's comments about how to represent metalanguage
within the KIF framework, and I believe that approach is sufficient
for any need that I have seen so far for any KR problems that we
have been looking at.

In response to Fritz's example from Peirce, I suggest the following
representation in conceptual graphs:

   If:    {*x}->(DFFR)->{*y}
   Then:  {Relation: *r}
          { (rho r)->{?x} ~{ (rho r)->{?y} } }- 
             (OR)-{ ~{ (rho r)->{?x} } (rho r)->{?y} }.


Comment on the notation:  This terminal I am using now does not have
square brackets, so I had to use curly braces for the concept boxes.
The Greek letter rho is the operator that allows the relation variable 
?r to be used in a relation position instead of the referent position.
See my paper in the ICCS'93 proceedings for some discussion of the rho
and tau operators and their use in metalanguage statements.

For those who may not be familiar with the CG notation, you can read
this graph as the English sentence "If x differs from y, then there exists
a relation r where either r applies to x and not to y or r does not applie
to x and it does apply to y."

I recently came across a book that people who are interested in this topic
may find useful:

   _Introduction to HOL:  A theorem proving environment for higher
   order logic_, edited by M. J. C. Gordon & T. F. Melham,
   Cambridge University Press, 1993.  ISBN 0 521 44189 7. $44.95

HOL is a theorem proving environment whose metalanguage is ML,
which is a very nice, clean functional programming language.
I happened to mention ML in a couple of earlier notes as a language
that is worth looking at for those people who want to represent
algorithms in logic.  ML is not really logic, but it is purely
functional and can be described in logic very nicely.


There are a couple of versions of HOL that can be obtained by FTP,
including a version of HOL88, which is implemented on top of LISP,
and a more efficient HOL90, which is implemented in ML, which is
compiled into machine language for various systems, including
Unix machines, Macintosh, and PC-compatibles.

The reason why I mention HOL is that it appears to use the same
kind of mechanisms that we are recommending for KIF and CGs.
Although the authors call their system HOL, I would call it a
version of FOL with a mechanism for supporting layers of metalanguages.
That is essentially what we are proposing for KIF and CGs.
  
I must admit that I have not used HOL myself, and I may be wrong in
my assessment of it.  But from looking at the book, I do not find
any "show stoppers" that we could not implement in KIF and CGs.
I do, by the way, see many very interesting ideas and techniques
that anyone in the CG or KIF communities should seriously consider
as useful approaches to implement on top of or inside of KIF and/or CGs.
HOL and ML have been around for some time and have a user community
and application experience that we should take advantage of for the
Knowledge Sharing Effort and for the ANSI and ISO conceptual schema work.

John Sowa