Project

Back to overview

Refining Reasoning via Justification Extraction: A Proof-Theoretic Approach

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

All Disciplines (2)

Discipline
Information Technology
Mathematics

Keywords (9)

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

Lay Summary (English)

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

Responsible applicant and co-applicants

Employees

Publications

Publication
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.
Logical Omniscience As Infeasibility
Artemov Sergei, Kuznets Roman (2014), Logical Omniscience As Infeasibility, in Annals of Pure and Applied Logic, 165(1), 6-25.
Realizing Public Announcements by Justifications
Bucheli Samuel, Kuznets Roman, Studer Thomas (2014), Realizing Public Announcements by Justifications, in Journal of Computer and System Sciences, 80(6), 1046-1066.
Decidability for Justification Logics Revisited
Bucheli Samuel, Kuznets Roman, Studer Thomas (2013), Decidability for Justification Logics Revisited, in Richter Frank, Bezhanishvili Guram , Marra Vincenzo , Löbner Sebastian (ed.), Springer, Berlin Heidelberg, 166-181.
Update as Evidence: Belief Expansion
Kuznets Roman, Studer Thomas (2013), Update as Evidence: Belief Expansion, in Nerode Anil, Artemov Sergei (ed.), Springer, Berlin Heidelberg, 266-279.
Justifications, Ontology, and Conservativity
Kuznets Roman, Studer Thomas (2012), Justifications, Ontology, and Conservativity, in Braüner Torben , Bolander Thomas , Moss Lawrence , Ghilardi Silvio (ed.), College Publications, London, 437-458.
Realization for Justification Logics via Nested Sequents: Modularity through Embedding
Goetschi Remo, Kuznets Roman (2012), Realization for Justification Logics via Nested Sequents: Modularity through Embedding, in Annals of Pure and Applied Logic, 163(9), 1271-1298.
Justifications for Common Knowledge
Bucheli Samuel, Kuznets Roman, Studer Thomas (2011), Justifications for Common Knowledge, in Journal of Applied Non-Classical Logics, 21(1), 35-60.
Partial Realization in Dynamic Justification Logic
Bucheli Samuel, Kuznets Roman, Studer Thomas (2011), Partial Realization in Dynamic Justification Logic, in de Queiroz Ruy, Beklemishev Lev (ed.), Springer, Berlin Heidelberg, 35-51.
TABLEAUX 2011: Workshops, Tutorials, and Short Papers
Giese Martin , Kuznets Roman (ed.) (2011), TABLEAUX 2011: Workshops, Tutorials, and Short Papers.

Collaboration

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

Scientific events

Active participation

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;


Self-organised

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
Workshop "Gentzen Systems and Beyond '11" 04.07.2011 Bern, Switzerland

Associated projects

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)

Abstract

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.
-