Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!mnetor!seismo!columbia!rutgers!ames!ucbcad!ucbvax!CSL.SRI.COM!MESEGUER
From: MESEGUER@CSL.SRI.COM (Jose Meseguer)
Newsgroups: mod.ai
Subject: Seminar - General Logic (SRI)
Message-ID: <8701190753.AA04797@ucbvax.Berkeley.EDU>
Date: Wed, 14-Jan-87 14:26:56 EST
Article-I.D.: ucbvax.8701190753.AA04797
Posted: Wed Jan 14 14:26:56 1987
Date-Received: Mon, 19-Jan-87 19:05:40 EST
Sender: daemon@ucbvax.BERKELEY.EDU
Organization: The ARPA Internet
Lines: 25
Approved: ailist@sri-stripe.arpa


                          GENERAL LOGIC

                               by

                         Prof. Gordon Plotkin
                 C.S. Dept. Univ. of Edinburgh, Scotland

WHEN: Thursday Jan. 15, at 1:30 pm
WHERE: SRI, Room AA298


   A wide variety of logics have been proposed for use in Computer
Science , such as first-order , higher-order , type theories , temporal and
modal logics , dynamic logic etc etc . One would like to write proof-checkers
and (semi-) automatic theorem provers for them , but implementing any one is 
a major undertaking and it is very hard to vary the logic once work is
underway . We propose a general syntactic theory of logic building on
work of Martin-Lof and employing a lambda calculus of dependent types.It
enables one to use a signature to enter the syntax and rules , in natural
deuction style. It seems likely to allow the efficient production of basic
proof checkers from  the signature and to provide the user the tools to
write theorem provers.

-------