Work Packages


The general scientific objective of this project is to develop a coordinated set of tools interweaving algebraic and proof theoretic methods in order to study substructural logics. To achieve this objective, the workload has been organized in work packages.

  • WP1: Management and organization

  • WP2: Dissemination and communication activities

  • WP3: Schools and training

  • WP4: General semantics and axiomatization

  • WP5: Correspondence theory and fixpoint logics

  • WP6: Proof-theory and complexity

  • WP7: Logics for special reasoning models

  • WP8: Logical analysis of natural language

WP1: Management and organization

The project management is the basic responsibility of the project coordinator assisted by the Steering Committee

WP2: Dissemination and communication activities

Dissemination and communication: organization of 3 conferences, organization of 5 workshops, 3 special session in international conferences, organization of 3 open lecture within the main conferences, preparation of 2 broad audience-oriented publications, managing the webpage and social media accounts

WP3: Schools and training

The main training events in the project will be the two schools, to be held at the at month 12 and month 24. Selected topics in theoretical and applied areas of substructural modal logics will be taught by members of the project. The schools will be held at some of the partner universities and will last one week. There will be from four to six researchers delivering lectures on topics of interest for both PhD and Master students. All the participant organisations have both lodging and conference facilities suitable to organise such events. Part of the funds will be devoted to support the expenses of international students

WP4: General semantics and axiomatization

Residuated lattices are the algebraic semantics for substructural logics. The overall aim of this work package is to study residuated lattices with modal operators, their dual relational frames, their structural properties. Further, we aim at studying the relational, frame, semantics within the general theory of coalgebras and investigating general axiomatization problems

WP5: Correspondence theory and fixpoint logics

Sahlqvist theorem and van Benthem’s charaterization theorem are seminal results in classical modal logic. Sahlqvist theorem allows completeness results to be proved ‘automatically’ using axioms of a special syntactic form. Logics with these axioms are always Kripke complete, and quite common, so the theorem is extremely powerful. Van Benthem’s characterization theorem states that modal logic can be identified with the bisimulation invariant fragment of first-order logic. Building on these methods we aim to expand the setting of both results to a new realm of substructural and many-valued logics. Many applications of modal logic, in particular in computer science, require the formalism to deal with various kinds of recursion. Modal fixpoint logics are extensions of basic modal logic that deal with the concept of recursion in an elegant and fundamental way by adding operators or connectives that can express recursive statements. Well-known examples include logics such as PDL, CTL and the modal μ- calculus. The interplay of nested fixpoints is the main cause of complexity in these systems, and only very recently some general methods have become available

WP6: Proof-theory and complexity

The main aim of this work package is the creation and application of different types of suitable calculi for substructural and related modal logics, in particular analytic and polynomial ring calculi, as well as natural deduction systems. Further, we investigate Depth-bounded modal logics, we investigate the computational complexity for the SAT problem for those decidable substructural modal logics

WP7: Logics for special reasoning models

In this work package we address the fourth specific objective of the project related to the development of an ample variety of non-classical modal formalisms from a more applied perspective, addressing di↵erent kinds of reasoning modes, namely reasoning about norms, temporal relations, preferences, uncertainty, discussions and resources. A particular task is to formalise and model information flow and reasoning based on probabilistic and contradictory information to study how to limit data collection and to characterise the sensitive information that can be deduced about the population based on the collected data

WP8: Logical analysis of natural language

(Multi)modal expansion of Lambek calculus are substructural modal logics aimed at processing the rules for constructing syntactically valid expressions of natural languages. The general aim of this objective is to determine new methods and to apply results previously obtained on substructural modal logic to the analysis of natural language