Mateus de Oliveira Oliveira


    • I’m the leader of the project “Automated Theorem Proving From the Mindset of Parameterized Complexity Theory” (AUTOPROVING). This is an 8 Million NOK project financed by the Research Council of Norway within the IKTPLUSS “Young Research Talents” program.
    • My main research interest is the application of techniques from computational logic, computational complexity theory and structural graph theory in the study of problems relevant to Artificial Intelligence and related areas. 


  • 2019-2023 – AUTOPROVING -Automated Theorem Proving from the Mindset of Parameterized Complexity Theory. Research Council of Norway (IKTPLUSS), Young Researchers Talent Grant (8 Million NOK).
  • 2020-2021 – Algorithmic Automata Theory: A Multivariate Approach. DAAD/RNC Mobility Program. The goal of this grant is to fund short-term visits of PhD students from the University of Bergen to the University of Trier (Germany). (100 Thousand NOK).

  • 2020-2021 – SPIRE Grant – The goal of this grant is to fund short term visits of international researchers to the University of Bergen. (63 Thousand NOK)

  • 2019-2019 – University of Bergen, Positioning Grant (50 Thousand NOK). The goal of this grant was to build international Collaboration. 


  • Farhad Vadiee – Ph.D. Student – University of Bergen. Farhad is working in my project AUTOPROVING. I’m Farhad main supervisor.

  • Emmanuel Arrighi – Ph.D. Student – University of Bergen. Emmanuel is working in Prof. Michael Fellow’s project “Parameterized Complexity of Practical Computing”. I’m one of Emmanuel’s co-supervisors.



  • Unitary Branching Programs: Learnability and Lower Bounds
    Fidel Andino, Maria Kokkou, Mateus de Oliveira Oliveira, Farhad Vadiee
    38-th International Conference on Machine Learning (ICML 2021) (accepted)

  • Diversity in Kemeny Rank Aggregation: A Parameterized Approach
    Emmanuel Arrighi, Henning Fernau, Daniel Lokshtanov, Mateus de Oliveira Oliveira, Petra Wolf
    30th International Joint Conference on Artificial Intelligence (IJCAI 2021) (accepted)

  • Three is Enough for Steiner Trees
    Emmanuel Arrighi, Mateus de Oliveira Oliveira
    19th Symposium on Experimental Algorithms (SEA 2021) (accepted)


  • Second-Order Finite Automata
    Alexsander Andrade de Melo, Mateus de Oliveira Oliveira
    15th International Computer Science Symposium in Russia (CSR 2020) (Invited Paper )




  • Parameterized Provability in Equational Logic
    Mateus de Oliveira Oliveira
    Proc. of the 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017).
    Brasília, Brazil, September 2017




Automated Theorem Proving from the Mindset of Parameterized Complexity Theory

The idea of proving or disproving mathematical statements using automated procedures has been contemplated for at least one century. Nevertheless, even though the field of automated reasoning has reached important milestones during the past few decades, the question of whether computers can significantly speed up the process of proof construction remains elusive.

The goal of this project is to identify a series of numerical parameters that are typically small in humanly produced proofs. Intuitively these parameters are intended to provide a numerical quantification of the complexity of a proof. Using information about these parameters, we will develop new algorithms that will be able to either find a proof of a given predetermined complexity or to determine that no such proof exists.

As a byproduct, we expect that our results will have the potential to improve significantly the automation capabilities of a variety of tools, such as proof assistants, software verification tools, specialist systems, etc.

Scroll to Top