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
Jäger Gerhard, Marti Michel (2016), A canonical model construction for intuitionistic distributed knowledge, in Advances in Modal Logic, Volume 11
, BudapestCollege Publications, Budapest.
Kokkinis Ioannis, Studer Thomas (2016), Cyclic proofs for linear temporal logic, De Gruyter, Berlin, Boston, 171-192.
Jäger Gerhard, Marti Michel (2016), Intuitionistic common knowledge or belief, in Journal of Applied Logic
, 18, 150-163.
Marti Michel, Studer Thomas (2016), Intuitionistic modal logic made explicit, in IfCoLog Journal of Logics and their Applications
, 3(5), 877-901.
Kokkinis Ioannis, Ognjanovic Zoran, Studer Thomas (2016), Probabilistic Justification Logic, in Logical Foundations of Computer Science LFCS 2016
, Springer, Cham.
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.
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.
Fitting Melvin, Kuznets Roman (2015), Modal interpolation via nested sequents, in Annals of Pure and Applied Logic
, 166(3), 274-305.
Kuznets Roman, Studer Thomas, Weak Arithmetical Interpretations for the Logic of Proofs, in Logic Journal of the IGPL
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.