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; Wed, 11 May 1994 11:46:58 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA17473; Wed, 11 May 1994 04:33:24 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from canopus.cc.umanitoba.ca by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA17469; Wed, 11 May 1994 04:33:22 -0600 Received: from eeserv.ee.UManitoba.CA by canopus.CC.UManitoba.CA (4.1/25-eef) id AA22896; Wed, 11 May 94 05:34:24 CDT Received: from ic16.ee.umanitoba.ca by eeserv.ee.UManitoba.CA (4.1/25a-eef) id AA27172; Wed, 11 May 94 05:34:22 CDT Received: by ic16.ee.umanitoba.ca (4.1/25-eef) id AA07914; Wed, 11 May 94 05:34:21 CDT From: rahard@ee.UManitoba.CA Message-Id: <9405111034.AA07914@ic16.ee.umanitoba.ca> Subject: temporal logics ? To: info-hol@leopard.cs.byu.edu Date: Wed, 11 May 1994 05:34:20 -0500 (CDT) X-Mailer: ELM [version 2.4 PL22] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 299 Hi, I am (a newbie) looking for references to express temporal logic in HOL. A tutorial would be better. (sorry if this question has been asked before) thanks, -- budi -- Budi Rahardjo Electrical Engineering - University of Manitoba - Canada