Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF

• Mail folder: SRKB Mail
• Next message: Fritz Lehmann: ""Contexts: logic-order for the CSMF standard""
• Previous message: Chris Menzel: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"
• In-reply-to: Fritz Lehmann: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"
• Reply: David McAllester: "INTERNATIONAL STANDARD FOR LOGIC: CSMF"
• Reply: Pat Hayes: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"

Date: Sun, 11 Sep 1994 03:18:38 -0700
From: John McCarthy <jmc@SAIL.Stanford.EDU>
Message-id: <9409111018.AA23545@SAIL.Stanford.EDU>
To: fritz@rodin.wustl.edu
Cc: dam@ai.mit.edu, tony@ontek.com, E.Hunt@cgsmtp.comdt.uscg.mil,
        bhacker@nara.gov, cg@cs.umn.edu, duschka@cs.stanford.edu,
        genesereth@cs.stanford.edu, interlingua@ISI.EDU, jksharp@sandia.gov,
        msingh@bcr.cc.bellcore.com, msmith@vax2.cstp.umkc.edu,
        roger@ci.deere.com, scott@ontek.com, sharadg@atc.boeing.com,
        skperez@mcimail.com, sowa@turing.pacss.binghamton.edu,
        srkb@cs.umbc.edu, fritz@rodin.wustl.edu
In-reply-to: <9409092205.AA01265@rodin.wustl.edu> (fritz@rodin.wustl.edu)
Subject: Re:  INTERNATIONAL STANDARD FOR LOGIC: CSMF
Reply-To: jmc@cs.stanford.edu
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk

   Date: Fri, 9 Sep 94 17:05:28 CDT
   From: fritz@rodin.wustl.edu (Fritz Lehmann)
   Cc: E.Hunt@cgsmtp.comdt.uscg.mil, bhacker@nara.gov, cg@cs.umn.edu,
	   duschka@cs.stanford.edu, genesereth@cs.stanford.edu,
	   interlingua@ISI.EDU, jksharp@sandia.gov, msingh@bcr.cc.bellcore.com,
	   msmith@vax2.cstp.umkc.edu, roger@ci.deere.com, scott@ontek.com,
	   sharadg@atc.boeing.com, skperez@mcimail.com,
	   sowa@turing.pacss.binghamton.edu, srkb@cs.umbc.edu,
	   uunet!rodin.wustl.edu!fritz@uunet.uu.net

	David McAllester pointed out that connectivity of
   graphs, which is not definable in First-Order semantics,
   is needed as a practical matter by designers and
   verifiers of circuit designs.  I would add that
   the same is true of planarity.  Planarity is not
   definable with First-Orderism, but it is very
   important in circuit design.  A planar subgraph
   of a circuit requires only one layer -- this
   reduced the number of physical layers in an
   integrated circuit chip, and the number of
   layers and drilled-through holes on a printed
   circuit board.  In IC manufacture, planarity is
   a multi-million-dollar predicate.


			     Yours truly,   Fritz Lehmann
   GRANDAI Software, 4282 Sandburg Way, Irvine, CA 92715, U.S.A.
   Tel:(714)-733-0566  Fax:(714)-733-0506  fritz@rodin.wustl.edu
   =============================================================


I take no position on whether higher order logic should be supplied.
However, David McAllester's statement is missing an important
qualification.  If the individual variables of a theory of graphs take
only the values of nodes of the graph, then planarity cannot be
defined.  However, if set theory is included in the first order
formalism, then planarity is should be definable.

My opinion, is that set theory should be used whatever the underlying
logi, and it can give the formal power of any higher order logic.
However, quantifying over predicates directly rather than having to
imitate them by sets is often (perhaps usually) more convenient.