# Re: Quoting and unquoting variables in KIF

schubert@cs.rochester.edu
Reply-To: cg@cs.umn.edu
Date: Mon, 12 Apr 93 15:24:18 -0400
From: schubert@cs.rochester.edu
Message-id: <9304121924.AA06544@ash.cs.rochester.edu>
To: schubert@cs.rochester.edu, sowa@turing.pacss.binghamton.edu
Subject: Re: Quoting and unquoting variables in KIF
Cc: cg@cs.umn.edu, interlingua@isi.edu

Well, your definition of propositions still allows statements related
by arbitrarily complex equivalence proofs to stand for the same
proposition (contrary to intuition). E.g., consider two statements of
form
(premises & conclusion),
(premises),
where "premises" is some conjunction of sentences and "conclusion"
is a sentence that follows from the premises by some enormously long
proof, and contains only predicates occurring in the premises. (The
mapping requirements you suggest are easy to satisfy here.)
-Len Schubert