Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id TAA25294; Mon, 23 Oct 1995 19:16:56 +0200 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA008052252; Mon, 23 Oct 1995 09:30:53 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: list Received: from bunsen.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA008022244; Mon, 23 Oct 1995 09:30:44 -0600 Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) by bunsen.cs.byu.edu (8.6.9/8.6.9) with ESMTP id JAA24180 for ; Mon, 23 Oct 1995 09:29:36 -0600 Received: from albatross.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 23 Oct 1995 15:25:57 +0000 X-Mailer: exmh version 1.6.4+cl+patch 10/10/95 To: cmere@omega.lncc.br (Maria Claudia Mere) Cc: info-hol@cs.byu.edu Subject: Re: HELP!! X-Uri: X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. In-Reply-To: Your message of Mon, 23 Oct 1995 11:18:04 -0200. <9510231318.AA25311@omega.lncc.br> Date: Mon, 23 Oct 1995 15:25:50 +0000 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:267530:951023152607"@cl.cam.ac.uk> > I am using the temporal logic S4.3.1 to specify Hypermedia applications, > actually the navegational behaviour of them. > A specification is a theory of first-order, two-sorted formulas in > such modal logic. We have also, equality for each sort. The proof assistant Isabelle supports a good many logics, including the modal logics T, S4 and S43. Although there is plenty of documentation on Isabelle itself, there is practically none on the Isabelle implementation of modal logic. It includes an automatic prover for modal logic but I know little about it. The inference system is based upon a sequent calculus devised by R. Gore. Isabelle and some documentation is available on the World Wide Web. For an introduction, please see http://www.cl.cam.ac.uk/Research/HVG/isabelle.html -- Larry Paulson