**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.