Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2011/12 / Oberseminar / Vivek Nigam,


Vivek Nigam,

TCS Oberseminar, 16.12.2011, 14:15 Uhr
Wann 14:15 15:15 16.12.2011
von bis
Wo L109
Termin übernehmen vCal

Vivek Nigam
A Framework for Specifying and Reasoning about Proof Systems

In this talk, I will introduce an on-going project whose objective is to build a framework that can facilitate the design and development of proof systems. In the first part of the talk, I will show how one can specify a wide number of proof systems in the logical framework called SELLF, which is based on linear logic with subexponentials. Then I will present novel techniques to reason automatically about proof systems. In particular, I will demonstrate how one can check automatically two important properties of proof systems, namely, whether a proof system admits cut-elimination and which inference rules of the encoded proof system permute over other rules. If time permits, I might run a demo on the latter application.


abgelegt unter: