Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Fri, 16 Apr 1993 14:55:11 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05415; Fri, 16 Apr 93 06:43:34 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05410; Fri, 16 Apr 93 06:43:27 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 16 Apr 1993 14:42:25 +0100 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list), Tom.Melham@uk.ac.cam.cl Subject: Re: Reports on Formalization of Temporal Logic? In-Reply-To: Your message of Fri, 16 Apr 93 12:07:07 +0100. <199304161007.AA05689@infix.cs.ruu.nl> Date: Fri, 16 Apr 93 14:42:18 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.926:16.04.93.13.42.39"@cl.cam.ac.uk> > I knew that Amit Jasuya has implemented Temporal Logic for HOL, and > that Ching-Tsun Chou is working on TLA. I wish to refer to their works > and others closely connected to formalization of temporal like logics. > Can someone post the bib-entry for the corresponding reports? Roger Hale did some work on the semantics of ITL (Interval Temporal Logic) in HOL. Reference: R.W.S. Hale, `Programming in Temporal Logic' (Ph.D. dissertation, University of Cambridge, 1988). Tom