**Mail folder:**Interlingua Mail**Next message:**Fritz Lehmann: "Higher-Order KIF and Conceptual Graphs"**Previous message:**Fritz Lehmann: "Higher-order KIF & Conceptual Graphs"**Reply:**sowa: "Higher-order logic"

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