Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05402-0@swan.cl.cam.ac.uk>; Fri, 19 Jun 1992 01:04:56 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10205; Thu, 18 Jun 92 16:55:31 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA10200; Thu, 18 Jun 92 16:55:24 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61c+YP/3.13) id AA29093; Thu, 18 Jun 92 16:56:11 -0700 Message-Id: <9206182356.AA29093@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs Subject: Temporal logic in HOL Date: Thu, 18 Jun 92 16:56:09 PDT From: chou@edu.ucla.cs I'd like to know the state of the art of embedding temporal logic in HOL. What are the papers to read? In particular, I wonder if anyone has used temporal logic in natural deduction or sequent calculus style. Your comments would be greatly appreciated. Cheers, Ching-Tsun Chou