**Mail folder:**SRKB Mail**Next message:**Fritz Lehmann: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"**Previous message:**John F. Sowa: "Re: CCAT Conceptual Catalogue and Ontologies"**In-reply-to:**Anthony K. Sarris: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"**Reply:**Fritz Lehmann: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"**Reply:**sowa: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"**Reply:**Chris Menzel: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"

From: dam@ai.mit.edu (David McAllester) Date: Fri, 9 Sep 94 17:06:07 EDT Message-id: <9409092106.AA03548@spock> To: tony@ontek.com Cc: fritz@rodin.wustl.edu, jksharp@sandia.gov, msmith@vax2.cstp.umkc.edu, sharadg@atc.boeing.com, roger@ci.deere.com, sowa@turing.pacss.binghamton.edu, msingh@bcr.cc.bellcore.com, bhacker@nara.gov, scott@ontek.com, tony@ontek.com, skperez@mcimail.com, genesereth@cs.stanford.edu, duschka@cs.stanford.edu, E.Hunt@cgsmtp.comdt.uscg.mil, cg@cs.umn.edu, interlingua@isi.edu, srkb@cs.umbc.edu In-reply-to: Anthony K. Sarris's message of Fri, 9 Sep 94 11:31:06 PDT <9409091831.AA01006@ontek.com> Subject: INTERNATIONAL STANDARD FOR LOGIC: CSMF Sender: owner-srkb@cs.umbc.edu Precedence: bulk

I have not generally taken part in interlingua discussions but have been generally concerned by the emphasis on first order semantics. It is well known, and stated in previous messages, that you can't even define the concept of "connected to" in a graph in first order logic. This has important PRACTICAL implications. Let Arc and Con be two binary relations and Phi(Arc, Con) be a formula which claims to state that Con(x,y) is true if and only if there is a path of arcs form x to y where Arc(x,y) means there is an arc from x to y. I challenge the supporters of a purely first order system to write this definition. When most people write Phi(Arc,Con) in first order logic they get something such that forall x P(x) ^ Arc(x,y) => P(y) plus Phi(Arc,Con) does NOT imply forall x P(x) ^ Con(x,y) => P(y). A concept language which can not define the concept of connected in a graph would seem to be of limited utility. As far as I'm concerned, the most important aspect of higher-order logic is support for context and other forms of modalization. Well, I would also like to be able to define "connected to". Internationally, there may well be objections to utilizing anything outside traditional FOL, as some national bodies have already expressed concerned that higher-order logics are simply too vaguely defined -- i.e., that they are largely the subject of research not general practice -- and are therefore not appropriate for inclusion or application within an ISO standard. The most widely used mechanical verification system is HOL, a mechanized fully higher order logic. HOL is more widely used, I believe, (in terms of actual number of users) than any mechanized first order system. The reason is simple --- first order systems do not provide sufficient expressive power to describe most of the concepts that hardware designers use, and most users of formal systems are currently hardware design verifiers. If KIF stays with first order semantics then I don't think that any hardware design team would ever select it for respresting hardware concepts. The simple concept of an n-bit ripple carry adder can not be expressed in first order logic. The problem, in practice, is mathematical induction. Many truths can only be proved if we have some form of induction principle. Induction principles are naturally second order. First order induction schemes are HARDER to compute with than higher order principles invoked with higher order matching and unification. Higher order unification may be bad, but wait till you try to use a first order induction scheme!. In summary, induction principles seem to be a necessity. Higher order induction principles seem more computationally tractable than first order induction schemes. If we try to sidestep the problem by using a first order syntax with an intended model, we will still need induction principles to reason about the standard model, so we are back where we started. David