Project

Back to overview

Structural proof theory and the logic of proofs

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
Show all

Keywords (12)

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

Lay Summary (English)

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

Responsible applicant and co-applicants

Employees

Publications

Publication
A Syntactic Realization Theorem for Justification Logics
Brünnler K., Goetschi R., Kuznets R. (2012), A Syntactic Realization Theorem for Justification Logics, in Advances in Modal Logic, Volume 8, College Publications, London.
Justifications for Common Knowledge
Bucheli S., Kuznets R., Studer T. (2011), Justifications for Common Knowledge, in Journal of Applied Non-classical Logics, 21(1), 35-60.
Partial Realization in Dynamic Justification Logic
Bucheli S., Kuznets R., Studer T. (2011), Partial Realization in Dynamic Justification Logic, in Logic, Language, Information and Computation, 18th International Workshop, WoLLIC 2011, Philadelphia?, ?.
Sequent Calculus for Justifications
Savateev Y. (2011), Sequent Calculus for Justifications, ?, Bern.
Explicit Evidence Systems with Common Knowledge
Bucheli S., Kuznets R., Studer T. (2010), Explicit Evidence Systems with Common Knowledge, arXiv.org, Cornell.
Justified Belief Change
Bucheli S., Kuznets R., Renne B., Sack J., Studer T (2010), Justified Belief Change, in Proceedings of the Second ILCLI International Workshop on Logic and Philosphy of Knowledge, Communic, ?University of the Basque Country Press, ?.
Self-Referential Justifications in Epistemic Logic
Kuznets R. (2010), Self-Referential Justifications in Epistemic Logic, in Theory of Computing Systems, 46, 636-661.
Two Ways to Common Knowledge
Bucheli S., Kuznets R., Studer T. (2010), Two Ways to Common Knowledge, in Proceedings of the 6th Workshop on Methods for Modalities (M4M–6 2009), CopenhagenElsevier, Amsterdam.
A Note on the Use of Sum in the Logic of Proofs
Kuznets R. (2009), A Note on the Use of Sum in the Logic of Proofs, in Proceedings of the 7th Panhellenic Logic Symposium, PatrasPatras University Press, Patras.
Logical Omniscience as a Computational Complexity Problem
Artemov S., Kuznets R. (2009), Logical Omniscience as a Computational Complexity Problem, in Theoretical Aspects of Rationality and Knowledge, TARK 2009, StanfordACM, ?.
The NP-completeness of reflected fragments of justification logics
Buss S.R., Kuznets R. (2009), The NP-completeness of reflected fragments of justification logics, in Proceedings of Symposium on Logical Foundations of Computer Science (LFCS'09), ??, ?.

Associated projects

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

-