LISA@XX.LCS.MIT.EDU (Lisa F. Melcher) (09/26/86)
Date: Thursday, October 2, 1986
Time: 1:45 p.m......Refreshments
Time: 2:00 p.m......Lecture
Place: NE43 - 512A
" GENERAL LOGIC "
Gordon Plotkin
Department of Computer Science
University of Edinburgh, Scotland
A good many logics have been proposed for use in Computer Science.
Implementing them involves repeating a great deal of work. We propose a
general account of logics as regards both their syntax and inference rules.
As immediate target we envision a system to which one inputs a logic
obtaining a simple proof-checker. The ideas build on work in logic of
Paulson, Martin-Lof and Schroeder-Heister and in the typed lambda-calculus of
Huet and Coquand and Meyer and Reinhold. The slogan is: Judgements are
Types. For example the judgement that a proposition is true is identified
with its type of proofs; general and hypothetical judgements are identified
with dependent product types. This gives one account of Natural Deduction.
It would be interesting to extend the work to consider (two-sided) sequent
calculi for classical and modal logics.
Sponsored by TOC, Laboratory for Computer Science
Albert Meyer, Host
-------MESEGUER@CSL.SRI.COM (Jose Meseguer) (01/14/87)
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.
-------