Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 8 Jul 1995 19:46:17 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA057137691; Sat, 8 Jul 1995 12:21:31 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from electra.cc.umanitoba.ca by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA057097687; Sat, 8 Jul 1995 12:21:27 -0600 Received: from eeserv.ee.umanitoba.ca (eeserv.ee.umanitoba.ca [130.179.8.1]) by electra.cc.umanitoba.ca (8.6.12/8.6.9) with SMTP id LAA28364 for ; Sat, 8 Jul 1995 11:06:43 -0500 From: rahard@ee.umanitoba.ca Received: from wine by eeserv.ee.umanitoba.ca (5.x/SMI-SVR4) id AA07125; Sat, 8 Jul 1995 11:04:50 -0500 Received: by wine (5.x/25-eef) id AA03789; Sat, 8 Jul 1995 11:03:02 -0500 Message-Id: <9507081603.AA03789@wine> Subject: [Q] manipulating assumptions To: info-hol@leopard.cs.byu.edu Date: Sat, 8 Jul 1995 11:03:02 -0500 (CDT) X-Mailer: ELM [version 2.4 PL24] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Question from a newbie: How do I manipulate assumptions? For example I have the following: "out = ~inp" 4 ["p1 = T" ] 3 ["~inp ==> (p1 = out)" ] 2 ["inp ==> (p2 = out)" ] 1 ["p2 = F" ] How do I rewrite assumption (2) assumption (1), and similarly rewrite assumption (3) with (4)? Actually I was trying to prove: "!inp out. (?p1 p2. (p1 = T) /\ (~inp ==> (p1 = out)) /\ (inp ==> (p2 = out)) /\ (p2 = F)) ==> (out = ~inp)" Sorry if this is to trivial for you. Thanks, -- budi -- Budi Rahardjo Electrical and Computer Engineering - University of Manitoba - Canada