#	Pagina
attuale pagina	/open-h2020/projects/195879/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - PAnaMoL (Proof-theoretic Analysis of Modal Logics)

Teaser

Summary

One of the most successful branches of modern symbolic logic is that of modal logics. Due to their favourable balance between expressivity and complexity, logics from this family have found many applications in disciplines such as Mathematics, Computer Science, Philosophy or Economics. In fact, modal logics are so successful that new specimens emerge almost on a daily basis. The downside of this is that often a lot of effort is spent reproving standard results for newly introduced logics. Hence there is a significant demand for general results about such logics, which could be easily instantiated for new specimens. Due to its independence of a particular semantics, the purely syntactic proof-theoretical approach is very promising in this regard.

With this in mind, the PAnaMoL project aimed at systematising proof theory for modal logics. We intended to provide a unified perspective on so-called sequent-style calculi and a deeper understanding of the general connections between modal axiom systems and sequent-style calculi for such logics. In detail the research objectives were:

The systematic development of suitable syntactic characterisations of modal axioms corresponding to natural formats of rules in different sequent-style frameworks.
A systematic comparison of the different sequent-style frameworks.
The exploitation of these results in: classification results stating necessary and sufficient proof-theoretic strength for important examples of logics; uniform decidability and complexity results for large classes of logics; general consistency proofs.

During the course of the project we established significant results towards these objectives. The resulting deeper understanding of the established proof-theoretic frameworks led to the identification of novel important proof-theoretic frameworks, the introduction of a number of general methods and techniques for the construction of suitable calculi for modal logics, and their application in the investigation of important classes of modal logics.

Work performed

First, we closely investigated the proof-theoretic framework of hypersequents and its relation to other proof-theoretic frameworks. This yielded, e.g., limitative results, stating that certain logics are not captured in the hypersequent framework, as well as positive results such as the first hypersequent-based decision procedure of optimal complexity for the important modal logic S5. Moreover, these investigations led to the introduction of the proof-theoretic framework of grafted hypersequents, which we used to provide novel complexity-optimal calculi for modal logics K5 and KD5.

A further investigation into the relations between other sequent-style calculi led to the introduction of the linear nested sequent framework, an intermediate framework between ordinary sequents and nested sequents. The introduction of this framework and the development of a new method for the construction of so-called standard calculi from ordinary sequent calculi was pivotal for the project. In particular, we used the developed method to construct novel modular calculi for an infinite class of multimodal non-normal and normal modal logics, based on classical or substructural propositional logic, and containing most of the standard logics. Investigating the connections between linear nested and labelled sequents yielded encodings of these calculi in linear logic. This included the surprising result that subexponential linear logic can be encoded in linear logic, and hence the two logics are equally expressive. Due to the modularity of the introduced calculi they naturally lend themselves to implementations. We heeded this call and implemented both the encoding of the calculi in a linear logic theorem prover as well as two theorem provers based directly on the calculi for the logics based on classical and substructural logic, respectively.

As an important application of the developed methods, in a series of publications we constructed novel standard calculi for a large class of conditional logics introduced by D. Lewis. Apart from giving rise to a practical decision procedure for the considered logics, the constructed calculi have a strong connection to the semantics of these logics, and thus can be used for counter model generation. A first implementation is available online.

The obtained results were disseminated in a number of scientific publications, both in international journals such as Theoretical Computer Science or the Logic Journal of the IGPL, and in the proceedings of renowned international conferences, such as TABLEAUX, JELIA, or LPAR.

Final results

The results obtained during the project significantly extended the state of the art in a number of ways.

In the hypersequent framework, while there were some limitative results concerning so-called structural hypersequent calculi for substructural and intermediate logics, our limitative results seem to be the first ones for hypersequent calculi with logical rules for modal logics. Moreover, so far hypersequent calculi were not considered suitable as a basis for complexity-optimal decision procedures. Our investigations into hypersequent calculi for S5 showed that in fact they are suitable for this.

The grafted hypersequent framework as a brand-new proof-theoretic framework will surely be of use as a tool in the search for complexity-optimal calculi for particular modal logics. As a case in point, while calculi for the modal logics K5 and KD5 had been established using nested sequents, our calculi are the first sequent-style calculi of optimal complexity for these logics. Moreover, they show that not the full power of the nested sequent framework is necessary for capturing these logics, and hence significantly contribute to a classification of these important examples. The developed calculi also were exploited in Kuznets: Interpolation method for multicomponent sequent calculi (2016) to obtain constructive proofs of interpolation.

The framework of linear nested sequents developed during the project provides an important clarification of the relationship between the ordinary sequents and nested sequents. Apart from serving as the basis for the introduction of nested sequent calculi for a large number of examples, the techniques for the construction of such calculi from ordinary sequent calculi provide a method for proving completeness of nested sequent calculi which is significantly simpler than previous approaches. As such it can be expected to have a significant impact.

The application of the developed methods in the construction of calculi for non-normal, multimodal, conditional and substructural modal logics significantly extended the reach of the nested sequent framework. While so far the received wisdom was that nested sequents were suitable mainly for normal modal logics, we opened up new horizons of applicability for this framework. In particular, our developed calculi for conditional logics are the first standard calculi for these logics, and the resulting implementation seems to be the first practical reasoning tool available for the considered logics.

In summary, the research conducted in the project will be of relevance to researchers in all fields where modal logics are used to model complex phenomena and provide easy-to-use results and methods for the proof-theoretic investigation and implementation of newly developed modal logics.