## Contact

Swiss National Science Foundation (SNSF)

Wildhainweg 3P.O. Box

CH-3001 Bern

Phone +41 31 308 22 22

Applicant | Kuznets Roman |
---|---|

Number | 131706 |

Funding scheme | Ambizione |

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

Institution of higher education | University of Berne - BE |

Main discipline | Information Technology |

Start/End | 01.01.2011 - 31.12.2013 |

Approved amount | 485'616.00 |

Discipline |
---|

Information Technology |

Mathematics |

modal logic; justification logic; structural proof theory; non-monotonic reasoning; Epistemic Logic; Sequent Calculus; Circularity; Logic of Proofs; Justification Extraction

Lead |
---|

Lay summary |

This project aims to extend the scope of Justification Logic to areas where traditionally Modal Logic has been applied---such as artificial intelligence, multi-agent systems, belief revision, dynamic epistemic logic, knowledge representation, program specification and verification, etc. Despite the popularity of the modal language, it has well-known drawbacks such as the Logical Omniscience Problem (agents know all logical truths and all logical consequence of their knowledge) and lacks expressivity to deal with the "Justified" part of the famous "Knowledge as Justified True Belief" paradigm. Justification Logic provides a solution by refining the language with syntactic objects that are interpreted as justifications (or proofs, or witnesses) and by introducing a formal machinery for handling them. The success of Modal Logic is due in part to its versatility: the modal language can be used to describe different phenomena by varying the axioms within the same language. Thus, it is necessary to provide a translation not only for the modal language in general, but also for individual theories in the modal language that are used in various applications. This process of translating modal reasoning into reasoning with justifications is called realization. Unfortunately, the applicability scope of the currently known realization algorithms is greatly narrowed by the fact that they require that the modal logic being translated have a purely syntactic and cut-free proof system. In particular, the most commonly used axiomatic, Hilbert-style representation of modal reasoning is not suitable for these realization algorithms. Since developing cut-free proof systems has proven to be difficult, this project proposes to develop new cut-tolerant realization techniques. A natural way of achieving this goal is by using the tools of structural proof theory: manipulating symbolic representations of proofs and devising algorithms for obtaining representations with required structural properties. The success of this project will allow automating justification extraction for a wide range of modal logics, especially those that resist cut elimination, including temporal modal logics and public announcement logics. |

Direct link to Lay Summary | Last update: 21.02.2013 |

Name | Institute |
---|

Name | Institute |
---|

Publication |
---|

Modal interpolation via nested sequents |

Logical Omniscience As Infeasibility |

Realizing Public Announcements by Justifications |

Decidability for Justification Logics Revisited |

Update as Evidence: Belief Expansion |

Justifications, Ontology, and Conservativity |

Realization for Justification Logics via Nested Sequents: Modularity through Embedding |

Justifications for Common Knowledge |

Partial Realization in Dynamic Justification Logic |

TABLEAUX 2011: Workshops, Tutorials, and Short Papers |

Group / person | Country |
---|

Types of collaboration |
---|

INRIA Research Centre Saclay - Île-de-France | France (Europe) |

- in-depth/constructive exchanges on approaches, methods or results |

Institute of Philosophy of the Academy of Sciences of the Czech Republic | Czech Republic (Europe) |

- in-depth/constructive exchanges on approaches, methods or results |

CUNY Graduate Center | United States of America (North America) |

- in-depth/constructive exchanges on approaches, methods or results - Publication |

Title | Type of contribution | Title of article or contribution | Date | Place | Persons involved |
---|

LIX Colloquium 2013 "Theory and Application of Formal Proofs" | Talk given at a conference | Craig Interpolation, Proof-Theoretically via Nested Sequents | 05.11.2013 | Palaiseau, France | Kuznets Roman; |

ABM12: Arbeitstagung Bern-München 2012 | Talk given at a conference | Constructive Interpolation for the Modal Cube Using Nested Sequents | 20.12.2012 | Munich, Germany | Kuznets Roman; |

Logical Models of Reasoning and Computation | Talk given at a conference | Realizing Public Announcements by Justifications | 01.02.2012 | Moscow, Russia | Kuznets Roman; |

ABM11: Arbeitstagung Bern-München 2011 | Talk given at a conference | Modal Interpolation via Nested Sequents | 15.12.2011 | Munich, Germany | Kuznets Roman; |

Workshop on Non-classical logics | Talk given at a conference | Modal Interpolation via Nested Sequents | 25.11.2011 | Vienna, Austria | Kuznets Roman; |

Prague Workshop on Epistemic Logics | Talk given at a conference | Logical Omniscience, Public Announcements and Justification Logic | 16.06.2011 | Prague, Czech Republic | Kuznets Roman; |

WoLLIC 2011: 18th Workshop on Logic, Language, Information and Computation | Talk given at a conference | Partial Realization in Dynamic Justification Logic | 18.05.2011 | Philadelphia, PA, United States of America | Kuznets Roman; |

Computational Logic Seminar at CUNY Graduate Center | Individual talk | Constructive Realization of Justification Logics via Nested Sequents | 17.05.2011 | New York, NY, United States of America | Kuznets Roman; |

Title | Date | Place |
---|

Advances in Proof Theory 2013 | 13.12.2013 | Bern, Switzerland |

LFCS 2013: Symposium on Logical Foundations of Computer Science (PC member) | 06.01.2013 | San Diego, CA, United States of America |

Explicit Paradigms in Logic and Computer Science | 04.06.2012 | Bern, Switzerland |

Workshop "Gentzen Systems and Beyond '11" | 04.07.2011 | Bern, Switzerland |

Tableaux 2011: The 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods | 04.07.2011 | Bern, Switzerland |

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

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

117699 | Structural proof theory and the logic of proofs | 01.05.2008 | Project funding (Div. I-III) |

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

Modal logic is a convenient way of formalizing a wide range of notions: permission/ obligation (deontic logic), time relations (temporal logic), knowledge (epistemic logic), belief (doxastic logic), etc. Although epistemic and doxastic modal logics are successfully used in artificial intelligence to model various modes of reasoning, agent interaction, and belief revision, there are also clear indications that in some instances of these applications modal language is not optimal. In such cases, justification logic has often proved useful in supplying the missing formal machinery. One of the weaknesses of epistemic modal logics, for instance, is the phenomenon of Logical Omniscience: agents whose reasoning abilities are described by modal principles unrealistically possess knowledge of all logical truths and of all logical consequences of the facts they know. Justification logic provides a more nuanced way of representing knowledge by introducing syntactic methods for handling justifications, which has proved fruitful in tackling the Logical Omniscience Problem. Modal language is also not expressive enough to faithfully capture the philosophical discussions about the nature of knowledge in mainstream epistemology, e.g., the discussions prompted by the famous Gettier examples that question the notion of knowledge as justified true belief, which can be traced back to Plato. In these examples, a belief is true and justified but the facts that make it true contradict the internal reasoning used by the agent to justify the belief; as a result, treating such a belief as knowledge seems counterintuitive. Where logical methods developed in formal epistemology remain powerless, justification language has succeeded in formalizing and analyzing these and similar epistemic paradoxes.While successes of justification logic in epistemic studies are encouraging, there is a serious obstacle that impedes further applications: the lack of a universal algorithm for justification extraction, i.e., for translating modal descriptions and arguments into a more precise language of explicit justifications. The existing justification extraction methods are highly sensitive to the formalism used to describe the laws of modal reasoning. Not only is a suitable formalism required, but it must also possess a valuable but rare property called cut-elimination (in the proofs-as-programs paradigm, the process of cut-elimination corresponds to program execution via an elimination of implicit descriptions; a mathematical analog is a removal of intermediate lemmas in a proof). While translating a modal argument into a suitable type of formalism rarely presents serious challenges, no general methods exist for designing formalisms that are cut-free.As a result, modeling with justifications currently relies on luck (the existence of a suitable cut-free formalism) or ad hoc tricks. Since a design of cut-free systems has remained elusive for more than half a century, the idea of this project is to develop new cut-tolerant techniques of justification extraction. A natural way of achieving this goal is to use the instrumentarium of structural proof theory: manipulating symbolic representations of proofs and devising algorithms for obtaining representations with required structural properties. In particular, studying modal proofs that are structurally suitable for justification extraction should pave way to concise and expressive sets of operations on justifications sufficient for representing various modes of reasoning, including non-monotonic reasoning.Equipped with general techniques of justification extraction, justification logic will become a reliable and handy tool in the arsenal of formal epistemology and will serve to strengthen the ties with its philosophical counterpart, mainstream epistemology. Further, the developed techniques will extend the reach of justification logic to temporal reasoning used in program verification, a development currently blocked by a lack of basic cut-free formulations for major temporal modal logics. The invigorated justification logic should prove an effective tool for studies in belief revision, knowledge representation, game theory, multi-agent systems, and automated proof search.

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