Xref: utzoo sci.logic:833 comp.lang.prolog:2790
Path: utzoo!attcan!uunet!mcsun!ukc!edcastle!lfcs!mikef
From: mikef@lfcs.ed.ac.uk (Mike Fourman)
Newsgroups: sci.logic,comp.lang.prolog
Subject: Re: Automated higher order logic
Message-ID: <4591@castle.ed.ac.uk>
Date: 8 Jun 90 13:29:52 GMT
References: <1990Jun7.164927.2631@ulrik.uio.no> <4571@castle.ed.ac.uk>
Reply-To: mikef@lfcs.ed.ac.uk (Mike Fourman)
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
Lines: 11

There are systems for computer-assisted proof in (various) higher-
order logic(s) under development and in use here at LFCS eg.
LEGO (Pollack)
LAMBDA (Abstract Hardwarte Ltd.)
ISABELLE (Paulson)


Prof. Michael P. Fourman                       email        mikef@lfcs.ed.ac.uk
Dept. of Computer Science                     'PHONE (+44) (0)31-667 1081 X2733
JCMB, King's Buildings                          FAX   (+44) (0)31 662 4712
Mayfield Road, Edinburgh EH9 3JZ, Scotland, UK