Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 17 Jun 1993 23:10:51 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16820; Thu, 17 Jun 93 15:04:59 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from linus.mitre.org by ted.cs.uidaho.edu (16.6/1.34) id AA16815; Thu, 17 Jun 93 15:04:54 -0700 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA13863; Thu, 17 Jun 93 18:05:15 -0400 Full-Name: Joshua D. Guttman Posted-Date: Thu, 17 Jun 93 18:05:12 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA03411; Thu, 17 Jun 93 18:05:13 -0400 Message-Id: <9306172205.AA03411@circe.mitre.org> To: David Parnas Cc: info-hol@ted.cs.uidaho.edu Subject: Re: Parnas: "some theorems we should prove" In-Reply-To: Your message of "Thu, 17 Jun 93 17:44:15 EDT." <199306172144.AA24996@qusunt.eng.McMaster.CA> X-Postal-Address: MITRE, Mail Stop A118 \\ 202 Burlington Rd. \\ Bedford, MA 01730 X-Telephone-Number: 617 271 2654; Fax 617 271 3816 Date: Thu, 17 Jun 93 18:05:12 -0400 From: guttman@linus.mitre.org In this case, where the candidate theorems are really quite explicit, I really only changed notation; and the change of notation was quite mechanical. The only point at which I had to think about your underlying semantics was in the discussion around page 4 where x=/=y was distinguished from not(x=y). This point actually worked out quite smoothly, as we use a logic in which P(t) is false when it is an *atomic* formula in which a non-denoting term t occurs as an immediate constituent. I inferred from what you wrote that this was also your semantics for formulas with non-denoting terms. As to automatic proof: our primary emphasis has been on interactive proofs, emphasizing mathematical theorems (of which some very substantial ones have been proved by my colleagues). However, almost half of your theorems were already proved automatically. I imagine that I could write a single "proof script" that would prove all those theorems (except the last) in a day or so. (And also many similar theorems.) The last is really a bit different because you need to use the fact that palindromes of length 1 are ubiquitous. But if the candidate theorem were "cooked" to indicate that 1 is the length to consider, then I think little more ingenuity would be involved there. If you'd like to read a bit about Imps, I would be happy to send you one or more papers. Joshua Guttman > > I would be curious to know what you mean by "formalizing" these theorems. > The formula in the paper looked formal to me. Do you mean something > more than changeing notation? > > We are of course looking for automatic proofs, not manually assisted > proofs. How far are you from that? > > >