## Contact

Swiss National Science Foundation (SNSF)

Wildhainweg 3P.O. Box

CH-3001 Bern

Phone +41 31 308 22 22

English title | Structural proof theory and the logic of proofs |
---|---|

Applicant | Jäger Gerhard |

Number | 117699 |

Funding scheme | Project funding (Div. I-III) |

Research institution | Institut für Informatik Universität Bern |

Institution of higher education | University of Berne - BE |

Main discipline | Information Technology |

Start/End | 01.05.2008 - 30.04.2011 |

Approved amount | 615'320.00 |

logic of proofs; proof polynomials; proof theory; sequent calculus; cutelimination; fixed points; cut-elimination; deep inference; modal logic; temporal logic; epistemic logic; cut elimination

Lead |
---|

Lay summary |

The Logic of Proofs was developed by S. Artemov in the nineties in orderto solve a problem posed by K. Gödel in the thirties. It is based onthe notion of a so-called "proof polynomial", which allows to talk aboutproofs inside of the logical language. Because of that it has foundnumerous applications in the areas of epistemic logic, verificationsystems and foundations of functional programming languages. Epistemiclogic is the study of knowledge. Here the Logic of Proofs allows toreason not only about knowledge, but also about the evidence from whichwe obtain the knowledge. Verification is used to ensure the correctnessof computational systems. Here the Logic of Proofs allows to reasonabout the correctness of the verifier itself. The Logic of Proofs alsoled to foundations of functional programming languages in which theexecution itself can be part of the program, in a certain sense.Even though the field has been growing rapidly, there still are areaswhich are not well understood. In particular, it is not known how todesign proof polynomials for logics with so-called "fixed points". Thisis unfortunate, because this includes important logics such as epistemiclogics with common knowledge and various temporal logics. Commonknowledge is a central concept in epistemic logic. It describes the factthat not only everybody knows a fact, but also everybody knows thateverybody knows this fact, and everybody knows that everybody knowsthat... and so on. That we should go at a green light and stop at a redlight, for example, is common knowledge among car drivers. Temporallogics, on the other hand, can reason about time and are central in theverification of the correctness of computational systems.The lack of proof polynomials for fixed points in particular means thatthere is no formal setting in which evidence-based knowledge and commonknowledge can be studied together. Also, there is no evidence-basedformal setting for reasoning about time. This is the first problem wewant to attack.Also, the relationship between proof polynomials and the so-called cutelimination is not well understood. Cut elimination is arguably the mostimportant operation on proofs. Crudely speaking it transforms a shortcreative proof into one that is long and not creative. Among many otherthings this ensures that proofs can be found even without creativity,such as by a computer. The study of cut elimination in the presence ofproof polynomials is the second problem we want to attack. |

Direct link to Lay Summary | Last update: 21.02.2013 |

Name | Institute |
---|

Name | Institute |
---|

Publication |
---|

A Syntactic Realization Theorem for Justification Logics |

Justifications for Common Knowledge |

Partial Realization in Dynamic Justification Logic |

Sequent Calculus for Justifications |

Explicit Evidence Systems with Common Knowledge |

Justified Belief Change |

Self-Referential Justifications in Epistemic Logic |

Two Ways to Common Knowledge |

A Note on the Use of Sum in the Logic of Proofs |

Logical Omniscience as a Computational Complexity Problem |

The NP-completeness of reflected fragments of justification logics |

Number | Title | Start | Funding scheme |
---|

134740 | Structural Proof Theory and the Logic of Proofs | 01.05.2011 | Project funding (Div. I-III) |

134740 | Structural Proof Theory and the Logic of Proofs | 01.05.2011 | Project funding (Div. I-III) |

131706 | Refining Reasoning via Justification Extraction: A Proof-Theoretic Approach | 01.01.2011 | Ambizione |

Swiss National Science Foundation (SNSF)

Wildhainweg 3P.O. Box

CH-3001 Bern

Phone +41 31 308 22 22

Enter and manage your applications

Enter your e-mail address to receive the SNSF Newsletter regularly

© SNSF 2018