INVESTIGADOR RESPONSÁVEL
Nome do Investigador Responsável (IR) do projeto da NOVA FCT: Isabel Oitavem
Contacto IR: oitavem@fct.unl.pt
Departamento: Matemática (DM)
UID: NOVA MATH
FINANCIAMENTO
Tipo de Financiamento: Privado
Entidade Financiadora: Royal Society
Referência da Call: International Exchanges 2026 Global Round 1
Referência: IES\R1\261049
Entidade proponente: Swansea University
Montante total do projeto: 12 000 libras - 14 048,46 euros (taxa de conversão a 30/09/2026)
Montante total para a NOVA: 12 000 libras - 14 048,46 euros (taxa de conversão a 30/09/2026)
Taxa de financiamento: 100%
PROJETO
Acrónimo: PACC
Título do Projeto: Proof-Theoretical Approaches to Computational Complexity
Data de início: 15/9/2026
Data de fim: 14/6/2028
Breve descrição do projeto:
A central goal in computer science is to understand why some problems are easy to solve while others seem hopelessly difficult—the famous P versus NP problem is the best-known example. Early approaches measured difficulty by the time or memory a computer needs, which was perceived as missing the mathematics of the problems themselves. A major shift occurred in 1974 when Ron Fagin showed that NP corresponds exactly to problems expressible in a particular logical language.
This revealed a powerful idea: the complexity of a problem is connected to the expressive power needed to describe it, not just the computational resources needed to solve it. Since then, many machineindependent characterisations of complexity classes have been developed. This project focuses on two such approaches—recursion theoretic and proof theoretic. Recursion theoretic work, as part of Implicit Computational Complexity (ICC), studies how restricted forms of defining functions can characterise classes like P. Proof theoretic work studies how the structure of logical systems corresponds to computational power. Two major frameworks here are Applicative Theories (AT) and Bounded Arithmetic (BA). AT offers a highly expressive setting for all computable functions, and complexity arises by limiting which proof principles are allowed. BA takes the opposite approach: it restricts the language itself so that only low complexity functions are expressible. This project brings AT and BA together with ICC to deepen our understanding of complexity classes. It aims at obtaining new characterisations of complexity by triangulating these areas through transfer of approaches.
