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 |