Re: FOL vs HOL vs MML
Ramesh Patil <ramesh@ISI.EDU>
Date: Sat, 11 Dec 1993 20:55:41 -0800
Message-id: <199312120455.AA24772@quark.isi.edu>
To: Matthew L. Ginsberg <ginsberg@cs.uoregon.edu>
From: Ramesh Patil <ramesh@ISI.EDU>
Subject: Re: FOL vs HOL vs MML
Cc: cg@cs.umn.edu, interlingua@ISI.EDU, sowa@turing.pacss.binghamton.edu
It appears to me that what Matt is asking for is reasonable. I would like
to see a formal proof for the claims of KIF/CG etc. being paradox free and
first order being submitted for peer review. Even better send them to Matt
and have him review it. I am sure Matt will be more than willing to review
them.
- Ramesh
>Amazing. A semantics with all the "practical" power of HOL but
>computationally equivalent to nested FOLs. I remember when things
>like this used to be subject to peer review and publication, as
>opposed to simply announced as standards.
>
>Anyway, to keep you from escaping the peer review process completely,
>I wonder if you could answer the following:
>
>(1) Do you have a proof that your MML cannot express paradoxes?
>I've asked this before and never gotten more than vague arguments;
>what I'm hoping for is a *proof*.
>
>(2) In your "practically equivalent" MML, do you have any way to
>express the fact that relation R' is exactly the transitive closure
>of relation R?
>
> Matt Ginsberg