PROALG

Proof-theoretic methods in algebra

 Partecipanti

Mappa

 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

 Obiettivo del progetto (Objective)

'The goal of this project is to develop and exploit proof-theoretic methods for ordered algebraic structures. Traditionally, algebra and proof theory represent two distinct approaches within logic: the former concerned with semantic meaning and structures, the latter with syntactic and algorithmic aspects. In many intriguing cases, however, methods from one field have been essential to obtaining proofs in the other. In particular, proof-theoretic techniques have been used to establish important results for classes of algebras in the framework of residuated lattices. This includes both algebras for a wide range of non-classical logics investigated across mathematics, computer science, philosophy, and linguistics, and also important examples from algebra such as lattice-ordered groups. In recent years, researchers from many countries have begun to explore connections between these two fields more closely, providing algebraic interpretations of proof-theoretic methods, and vice versa. The time is now ripe to clarify and exploit these connections.

The concrete objectives of the project are: (A) to define uniform proof systems for classes of algebras and logic (such as e.g., lattice-ordered groups or cancellative residuated lattices) not covered by known frameworks, (B) to use proof systems to establish new decidability and complexity results, (C) to investigate relationships between the algebraic property of amalgamation and the logical property of interpolation and use proof systems to settle open problems, (D) to use proof systems to establish correspondences between algebraic properties and admissible rules. The main challenge and originality of the project will be to combine new insights and techniques from algebra and proof theory to tackle these goals.'

Introduzione (Teaser)

Algebra and proof theory have traditionally developed in parallel, non-intersecting ways. However, an EU-funded project identified connections between these two areas of mathematics with exciting applications to computer science.

Descrizione progetto (Article)

Researchers decided it was not sufficient to compare the results of the two different approaches to establish the connection between algebra and proof theory. Therefore, it was necessary to apply methods and techniques from each field to obtain proofs in the other. The new discipline that emerged from the 'Proof-theoretic methods in algebra' (PROALG) project was named algebraic proof theory.

Under the auspices of the PROALG project, mathematicians from across the world pooled their efforts. Some provided expertise in proof theory, where proofs are represented as mathematical formulas with logical structure that can be analysed. Others contributed with their extensive experience in algebraic structures, consisting of elements bound by operators which satisfy certain of axioms.

The question that they all faced was what proofs will a given formula have, if it is provable? During the course of the PROALG project, scientists searched for and found proofs for algebraic structures such as partially ordered groups. They also used them to obtain proofs for fundamental theorems of each class of algebraic structures.

The relationship found between algebra and proof theory was then used for a thorough mathematical analysis of fuzzy logic rules. The structures in fuzzy logic attempt to capture the fuzziness' or imprecision of the real world, something that classical mathematics touches on through probability theory. The PROALG scientists were successful in defining new calculus proofs to capture uncertainty and necessity.

The development of analytic calculus proofs for fuzzy logic and other kinds of non-classical logic, was not only a theoretical task for the PROALG project. Besides establishing their fundamental properties, including consistency and computational complexity, it is key to their applications. The calculus proofs proceed by breaking down formulas step by step. This methodology is a prerequisite for the automatisation of proof search.

Through the close connections with computer science, algebraic proof theory is expected to contribute to research areas outside traditional mathematics. Among others, the new theory can contribute to the verification of computer programs. The key findings of the PROALG project were shared with the research community in eight journal papers and conference presentations.