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 153169
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.2014 - 30.04.2017
Approved amount 456'798.00
Show all

All Disciplines (2)

Discipline
Information Technology
Mathematics

Keywords (12)

proof polynomials; modal logic; logic of proofs; proof theory; sequent calculus; belief revision; public announcement logic; epistemic logic; intuitionistic logic; temporal logic; fixed points; cut-elimination

Lay Summary (German)

Lead
Die sogenannte Logic of Proofs ist ursprünglich von S. Artemov eingeführt worden, um ein lange offenen Problem im Zusammenhang mit der klassischen Beweisbarkeitssemantik der intuitionistischen Logik zu lösen. Die Hauptidee dieses Ansatzes besteht darin, Beweispolynome in die Objektsprache zu integrieren, um damit die Struktur von Beweisen (bis zu einem gewissen Grad) repräsentieren zu können. Dieser Ansatz hat sich als sehr erfolgreich herausgestellt und zur formalen Analyse von Beweisstrukturen zum Beispiel im Kontext der modalen Logik (mit Selbstreferentialität) und epistiemischer Paradoxien sowie im Zusammenhang mit dem Omniscience-Problem geführt.
Lay summary

Im Rahmen des vorliegenden Projekts verwenden wir diesen erweiterten logischen Formalismus auf einige Bereiche, die für die Informatik relevant sind. Dabei legen wir das Schwergewicht auf temporale Logiken, die häufig in Kontext von reaktiven Systemen eingesetzt werden, auf Belief Revision, common Knowledge sowie epistemische Logiken, die sich mit dynamischen Mehragentensystemen befassen. ausserdem beginnen wir mit der Untersuchung von Fixpunkttheorien über intuitionistischen modalen Systemen.


Direct link to Lay Summary Last update: 28.03.2014

Responsible applicant and co-applicants

Employees

Publications

Publication
A canonical model construction for intuitionistic distributed knowledge
Jäger Gerhard, Marti Michel (2016), A canonical model construction for intuitionistic distributed knowledge, in Advances in Modal Logic, Volume 11, BudapestCollege Publications, Budapest.
Cyclic proofs for linear temporal logic
Kokkinis Ioannis, Studer Thomas (2016), Cyclic proofs for linear temporal logic, De Gruyter, Berlin, Boston, 171-192.
Intuitionistic common knowledge or belief
Jäger Gerhard, Marti Michel (2016), Intuitionistic common knowledge or belief, in Journal of Applied Logic, 18, 150-163.
Intuitionistic modal logic made explicit
Marti Michel, Studer Thomas (2016), Intuitionistic modal logic made explicit, in IfCoLog Journal of Logics and their Applications, 3(5), 877-901.
Probabilistic Justification Logic
Kokkinis Ioannis, Ognjanovic Zoran, Studer Thomas (2016), Probabilistic Justification Logic, in Logical Foundations of Computer Science LFCS 2016, Springer, Cham.
The complexity of non-iterated probabilistic justification logic
Kokkinis Ioannis (2016), The complexity of non-iterated probabilistic justification logic, in International Symposium on Foundations of Information and Knowledge Systems FoIKS 2016, Springer, Cham.
First steps towards probabilistic justification logic
Kokkinis Ioannis, Maksimovic Petar, Ognjanovic Zoran, Studer Thomas (2015), First steps towards probabilistic justification logic, in Logic Journal of the IGPL, 23(4), 662-687.
Modal interpolation via nested sequents
Fitting Melvin, Kuznets Roman (2015), Modal interpolation via nested sequents, in Annals of Pure and Applied Logic, 166(3), 274-305.
Weak Arithmetical Interpretations for the Logic of Proofs
Kuznets Roman, Studer Thomas, Weak Arithmetical Interpretations for the Logic of Proofs, in Logic Journal of the IGPL.

Collaboration

Group / person Country
Types of collaboration
Research Laboratory for Logic and Computation, CUNY Graduate Center United States of America (North America)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
Laboratoire d'Informatique, INRIA Saclay - Île-de-France France (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
Steklov Mathematical Institute and Lomonosov Moscow State University Russia (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
Institute for Logic, Language and Computation, University of Amsterdam Netherlands (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Publication

Scientific events

Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
Logic and Applications 2016 Talk given at a conference Justification with Propositional Nominals 19.09.2016 Dubrovnik, Croatia Kashev Alexander;
Proofs, Justification and Certificates Talk given at a conference Justification Logic 03.06.2016 Toulouse, France Studer Thomas;
Arbeitstagung Bern München Talk given at a conference The Satisfiability Problem in Probabilistic Justification Logic 26.05.2016 Bern, Switzerland Kokkinis Ioannis;
Various Aspects of Modality Talk given at a conference Justification Logic 10.05.2016 Esfahan, Iran Studer Thomas;
Various Aspects of Modality Talk given at a conference The Proof Theory of Common Knowledge 10.05.2016 Esfahan, Iran Studer Thomas;
Seminar of the Department of Software Engineering, ORT Braude Academic College of Engineering Individual talk Probabilistic Justification Logic 12.04.2016 Karmiel, Israel Kokkinis Ioannis;
Interdisciplinary Lab for Intelligent and Adaptive Systems, Luxembourg Individual talk Justification Logic 22.03.2016 Luxemburg, Luxembourg Studer Thomas;
Foundations of Information and Knowledge Systems, Talk given at a conference The Complexity of Non-Iterated Probabilistic Justification Logic 10.03.2016 Linz, Austria Kokkinis Ioannis;
Logical Foundations of Computer Science Talk given at a conference Probabilistic Justification Logic 04.01.2016 Deerfield Beach, United States of America Studer Thomas;
Non-Classical Logics and Paradox II Talk given at a conference Introduction to Justification Logic 30.10.2015 Bern, Switzerland Studer Thomas;
Logic and Information Talk given at a conference Probabilistic Justification Logic 15.10.2015 Münchenwiler, Switzerland Kokkinis Ioannis;
Logic and Applications Talk given at a conference Probablistic Justification Logic 23.09.2015 Dubrovnik, Croatia Kokkinis Ioannis;
Logic Colloquium Talk given at a conference First Steps towards Probabilistic Justification Logic 05.08.2015 Helsinki, Finland Kokkinis Ioannis;
Universal Logic Talk given at a conference Probabilistic Justification Logic 25.06.2015 Istanbul, Turkey Studer Thomas;
Seminar for Probability Logic, Mathematical Institute of Serbian Academy of Sciences and Arts Individual talk Justification Logic 04.06.2015 Belgrad, Serbien Studer Thomas;
Center for Mathematics and Statistics: General Seminar, University of Novi Sad Individual talk Modal Logic - an Introduction 02.06.2015 Novi Sad, Serbien Studer Thomas;
Arbeitstagung Bern München Talk given at a conference First Steps towards Probabilistic Justification Logic 18.12.2014 München, Germany Kokkinis Ioannis;
Journée Logique Talk given at a conference Proofs and Fixed Points 02.12.2014 Marseille, France Studer Thomas;
Logic and Information Talk given at a conference First Steps towards Probabilistic Justification Logic 15.10.2014 Münchenwiler, Switzerland Kokkinis Ioannis;
Logic Colloquium Talk given at a conference Weak Arithmetical Semantics for the Logic of Proofs 14.07.2014 Wien, Austria Studer Thomas;
Gentzen Systems and Beyond Talk given at a conference On Cuts and Cut-Elimination in Modal Fixed Point Logics 13.07.2014 Wien, Austria Studer Thomas;


Awards

Title Year
JAACS Alumni Prize for the best doctoral thesis in computer science. JAACS is the Alumni Association of the three Computer Science Institutes IAM, IIUN and DIUF of the Universities of Bern, Neuchâtel, and Fribourg. 2016
Paul Bernays Award The Swiss Society for Logic and Philosophy of Science (SSLPS) awards each year the Paul Bernays Award to a young researcher for an outstanding contribution in the area of logic and philosophy of science. The award is sponsored by Altonaer Stiftung für philosophische Grundlagenforschung. 2016

Associated projects

Number Title Start Funding scheme
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
165549 Justifications and non-classical reasoning (Juno) 01.10.2016 Project funding (Div. I-III)

Abstract

The Logic of Proofs has been introduced by Artemov to solve a long-standing problem of a classical provability semantics for intuitionistic logic. The main idea of his approach was to introduce proof polynomials into the object language in order to represent the structure of proofs. The idea has proved itself fruitful and resulted in the formal study of proof structure in this and other contexts, including self-referentiality of modal reasoning, epistemic paradoxes, and logical omniscience problem.In this proposal, we continue expanding the benefits of using the more expressive language of the Logic of Proofs to various areas of computer science, focusing on temporal logics, traditionally used for describing properties of reactive systems, and belief revision, which studies operations for changing agents' beliefs in accordance with new information. We also continue our investigation of the applications of proof polynomials to logics of common knowledge and dynamic epistemic logics, which describe internal epistemic attitudes of rational agents and groups of agents in static and dynamic epistemic scenarios.The new Track B of this proposal sets forth a foundational study of fixed points in the constructive modal framework. While both intuitionistic modal logics and modal mu-calculus have received attention from the scientific community (the latter more than the former), there is virtually no study on constructive modal fixed-points, making the line of investigations proposed in Track B pioneering in this respect.
-