Campus Event Calendar
Event Entry
What and Who
Adding a validity primitive to a logical framework
Seán Matthews
MPII
AG2 Working Group Seminar
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 30 April 97
11:15
60 Minutes
46.1 - MPII
022
Saarbrücken
Abstract
Logical frameworks such as the Edinburgh LF or Isabelle have concentrated on the traditional logics of mathematical practice, i.e. classical or intuitionistic, propositional, or first- or higher-order logics, which can be given effective encodings in terms of some notion of `truth' consequence. Other logics, however, such as modal logics, introduce intensional elements that can really only be understood in terms of validity.
We discuss how one might extend a traditional logical framework of implies/forall with a new intensional logical connective for validity, which we can use to encode these logics directly.
Contact
Uwe Waldmann
--email hidden
passcode not visible
logged in users only