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.

Down below you will find a table with the project’s deliverables.

WP1 Management
WP2 Scientific events and outreaching activities
WP3 Schools
WP4 Abstract Algebraic Logic
WP5 Analytic Calculi
WP6 Structure Theory
WP7 Canonical Formulas
WP8 Dualities
WP9 Residuated lattices with operators

WP1 – Management
Leading group: UNISA.

All partecipants are involved in this WP, which is mainly devoted to logistic tasks. The main tasks are: organization of meetings to discuss the development of the project and satellite initiatives; maintaining the project web site; managing project document; preparing the progress reports; resolving any technical or administrative issue that is not addressed by other means during the project.


WP2 – Scientific events and outreaching activities
Leading groups: IIIA, UAB, CLE.

To maximize the outreaching potential of the project, we plan to prepare of two broad audience-oriented papers and to organise two conferences, that shall include “open lectures” given by senior scientists and oriented to the general public as well as press conferences prior the meeting. Moreover, we intend to organise four workshops, with the aim of maximising the interactions among partners and promote cross-fertilisation within and from outside the scheme and disseminate our results.


WP3 – Schools
Leading group: UNIBE.

We plan to organize two schools. Leading experts will teach selected topics in proof theory, abstract algebraic logic, residuated lattices, many-valued logic, etc.  There will be from four to six researchers delivering lectures on topic at the boundary of research, in such a way to be of interest both for PhD and Master students. The schools will be held at some of the partner universities and will last one week.


WP4 – Abstract Algebraic Logic
Leading groups: UTIA, USTINF. 

The global objective of this Work Package is to advance the state of the art in Abstract Algebraic logic. The plan is to develop a theory of translations between logics and to investigate equationally orderable quasivarieties and their associated sequent calculi and deductive systems. We intend to explore the relations between deduction theorems, proof by cases and filter generation, to study finite and infinite Beth’s definability for abstract logics, to provide a uniform framework for non-classical predicate logics and their model theory, and to investigate consequence relations with multisets of premises and conclusions.


WP5 – Analytic calculi for substructural logics
Leading group: TU.

The main aim of this work package is the creation and application of analytic calculi in substructural and related logics. We will focus on the following issues: using analytic calculi to obtain meta-logical results such as decidability, interpolation, conservativity, standard completeness and algebraic completions; developing new analytic calculi for substructural and related logics using existing proof-frameworks, especially the sequent calculus, hypersequent, nested sequent and display calculi, and via the introduction of new proof-frameworks.


WP6 – Structure Theory of Residuated Lattices
Leading groups: UNICA, UPOL.

We intend to develop the algebraic machinery needed for a deeper understanding of the structure of residuated lattices. To do so, plan to prove representations of residuated lattices in the style of “triple construction” and in the style of “Kites”, inspired by Stone algebras in the former case, and by the work of Jipsen and Montagna and the generalization of Dvurecenskij and Kowalski in the latter. We also plan to investigate divisible pseudo BCK-algebras and implement Conrad’s program for residuated lattices, investigating lateral completions of residuated lattices and using information about convex subalgebras to establish a categorical equivalence for integral GMV algebras.


WP7 – Canonical Formulas and Bounded proofs
Leading group: UVA.

We will concentrate on two fundamental concepts: axiomatization and robustness of proof systems. We intend to extend the technique of canonical formulas to substructural logics and residuated lattices, with the final aim of developing automated reasoning methods. We plan to develop the method in two directions: we will attempt to extend the method to logical formalisms such as substructural logics and we will try to extend the scope of the proof theory that it covers, in particular, by dealing with hypersequents. As a result, we intend to provide a completely new algebraic method for axiomatization and for verifying robustness of proof systems.


WP8 – Duality theory with algorithmic applications
Leading group: UNIMI.

This work package intends to address issues related to duality theory. Our first goal is to clarify the relationships between residuated frames and residuated lattices, establishing to what extent residuated frames can be considered as the objects dual to residuated lattices. We also intend to continue the investigation of a general theory of canonical extensions for algebras in the varieties corresponding to substructural logics and at exploring in depth the connection between join-completions and partial embeddings in the framework of residuated lattices.


WP9 – Residuated lattices with operators and alternative consequences
Leading group: CONICET.

The aim of this work package is to study the algebraic semantics of modal extensions of substructural logics, mainly those whose algebraic semantics are classes of commutative, bounded and integral residuated lattices. We want to investigate at large to what extent well known results on BAOs generalise to residuated algebras with operators (RLOs), addressing issues like representation theorems, the duality connection to relational semantics based on many-valued Kripke frames, etc. We will also focus on the problem of algebraizability of different modal extensions with new rules, as well as specific subclasses of RLOs and connect them to the corresponding logics given by Hilbert-style modal systems.


Table of deliverables

Name Type Associated WP Deadline Leading group
D1.2 Progress Report WP1 28/02/2017 UNISA
D2.1 Conference proceedings WP2 31/08/2016 CSIC
D2.2 Report of the first workshop WP2 30/04/2017 UMIL
D2.3 Second Workshop report WP2 30/06/2017 New Mexico State University
D2.4 Third workshop report WP2 31/01/2018 TU
D2.5 Fourth workshop WP2 31/08/2018 Nayang Technological University
D2.6 Final conference WP2 28/02/2019 CSIC
D3.1 Report on the first school WP3 30/06/2017 UP
D3.2 Report on the second school WP3 31/05/2018 UNICA
D4.1 Technical report WP4 31/10/2017 USTINF
D5.1 Technical report WP5 30/06/2018 TU
D6.1 Technical report WP6 31/07/2018 UNICA
D7.1 Technical report WP7 31/07/2018 UVA
D8.1 Technical report WP8 30/09/2018 UMIL
D9.1 Technical report WP9 31/01/2019 CONICET