Tata Institute of Fundamental Research
A Logic of Interactive Proofs
Seminar
Speaker:
Simon Kramer
University of Luxembourg
Interdisciplinary Centre for
Security and Trust Campus
Kirchberg, F103 6, rue
Richard Coudenhove-
Kalergi 1359
Luxembourg
Date:
Monday, 19 Dec 2011, 11:30 to 12:30
Venue:
AG-80
(Scan to add to calendar)
Abstract:
We propose a logic of interactive proofs as the first and main step towards an intuitionistic foundation for interactive computation to be obtained via an interactive analog of the Godel Kolmogorov-Artemov definition of intuitionistic logic as embedded into a classical modal logic of proofs, and of the Curry-Howard isomorphism between intuitionistic proofs and typed programs. Our interactive proofs effectuate a persistent epistemic impact in their intended communities of peer reviewers that consists in the induction of the (propositional) knowledge of their proof goal by means of the (individual) knowledge of the proof with the interpreting reviewer. That is, interactive proofs effectuate a transfer of propositional knowledge -- (to-be-)known facts -- via the transfer of certain individual knowledge -- (to-be-)known proofs -- in multi-agent systems. In other words, we as a community have the formal common knowledge that a proof is that which if known to one of our peer members would induce the knowledge of its proof goal with that member.
| Speaker: | Simon Kramer University of Luxembourg Interdisciplinary Centre for Security and Trust Campus Kirchberg, F103 6, rue Richard Coudenhove- Kalergi 1359 Luxembourg |
| Date: | Monday, 19 Dec 2011, 11:30 to 12:30 |
| Venue: | AG-80 |
(Scan to add to calendar)
Abstract:
We propose a logic of interactive proofs as the first and main step towards an intuitionistic foundation for interactive computation to be obtained via an interactive analog of the Godel Kolmogorov-Artemov definition of intuitionistic logic as embedded into a classical modal logic of proofs, and of the Curry-Howard isomorphism between intuitionistic proofs and typed programs. Our interactive proofs effectuate a persistent epistemic impact in their intended communities of peer reviewers that consists in the induction of the (propositional) knowledge of their proof goal by means of the (individual) knowledge of the proof with the interpreting reviewer. That is, interactive proofs effectuate a transfer of propositional knowledge -- (to-be-)known facts -- via the transfer of certain individual knowledge -- (to-be-)known proofs -- in multi-agent systems. In other words, we as a community have the formal common knowledge that a proof is that which if known to one of our peer members would induce the knowledge of its proof goal with that member.