Mateus de Oliveira Oliveira


Presentation

    • 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 interests are computational complexity theory, logic, and structural graph theory.

Grants


  • 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. 

Students

  • 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.

Publications

 

2021

  • 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)

2020

  • Diversity of Solutions: An Exploration Through the Lens of Fixed-Parameter Tractability Theory Julien Baste, Michael R. Fellows, Lars Jaffke, Tomáš Masařík, Mateus de Oliveira Oliveira, Geevarghese Philip, Frances A. Rosamond
    29th International Joint Conference on Artificial Intelligence (IJCAI 2020)

  • Satisfiability of Symbolic Constraint Satisfaction Problems Parameterized by Width
    Alexsander Andrade de Melo, Mateus de Oliveira Oliveira
    17th International Conference on Principles of Knowledge Representation and Reasoning (KR2020) (Accepted)

  • Width Notions for Ordering-Related Problems
    Emmanuel Arrighi, Henning Fernau, Mateus de Oliveira Oliveira, Petra Wolf
    40th Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020) (Accepted)

  • Compressing Permutation Groups into Grammars and Polytopes. A Graph Embedding Approach
    Lars Jaffke, Mateus De Oliveira Oliveira, Hans Raj Tiwary
    45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020) (Accepted)

  • Succinct Monotone Circuit Certification: Planarity and Parameterized Complexity
    Mateus Alves, Mateus De Oliveira Oliveira, Janio Silva and Uéverton Souza
    26th International Computing and Combinatorics Conference (COCOON 2020)

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

  • On the Fine-Grained Complexity of Finite Automata Non-Emptiness of Intersection
    Mateus de Oliveira Oliveira, Michael Wehar
    24th International Conference on Developments in Language Theory (DLT 2020)

  • Revisiting the Parameterized Complexity of Maximum-Duo Preservation String Mapping.
    Christian Komusiewicz, Mateus de Oliveira Oliveira, Meirav Zehavi.
    Theoretical Computer Science 847: 27-38. 2020
    Obs: Conference version appeared at CPM 2017.

2019

  • Representations of Monotone Boolean Functions by Linear Programs
    Mateus de Oliveira Oliveira, Pavel Pudlák
    ACM Transactions on Computation Theory. 11(4): 22:1-22:31. 2019
    Obs: conference version appeared at CCC 2017.

  • On the Width of Regular Classes of Finite Structures
    Alexsander Andrade de Melo, Mateus de Oliveira Oliveira
    27th International Conference on Automated Deduction (CADE 2019).
    Natal, Brazil, August 2019.

  • Type Inhabitation in Simply Typed Lambda Calculus Parameterized by Width
    Mateus de Oliveira Oliveira
    25th International Conference on Types for Proofs and Programs (TYPES 2019).
    Oslo, Norway, June 2019.

2018

  • Size-Treewidth Tradeoffs for Circuits Computing the Element Distinctness Function
    Mateus de Oliveira Oliveira
    Theory Comput. Syst. 62(1): 136-161 (2018).
    Obs: conference version appeared at STACS 2016.

  • A Strongly-Uniform Slicewise Polynomial-Time Algorithm for the Embedded Planar Diameter Improvement Problem
    Daniel Lokshtanov, Mateus de Oliveira Oliveira, Saket Saurabh
    Proc. of the 13th International Symposium on Parameterized and Exact Computation (IPEC 2018).
    Helsinki, Finland, August 2018.

  • Intersection Non-Emptiness and Hardness within Polynomial Time
    Mateus de Oliveira Oliveira, Michael Wehar
    Proc. of the 22nd International Conference on Developments in Language Theory (DLT 2018).
    Tokyo, Japan, September 2018.

  • Graph Amalgamation under Logical Constraints
    Mateus de Oliveira Oliveira
    Proc. 44th International Workshop on Graph-Theoretic Concepts in Computer Science (WG 2018).
    Cottbus, Germany, June 2018.

  • On Weak Isomorphism of Rooted Vertex-Colored Graphs
    Lars Jaffke, Mateus de Oliveira Oliveira
    Proc. of the 44th International Workshop on Graph-Theoretic Concepts in Computer Science (WG 2018).
    Cottbus, Germany, June 2018.

  • A Near-Quadratic Lower Bound for the Size of Quantum Circuits of Constant Treewidth
    Mateus de Oliveira Oliveira
    Proc. of the 29th ACM-SIAM Symposium on Discrete Algorithms (SODA 2018).
    New Orleans, Louisiana, USA, January 2018.

2017

  • 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

  • On Supergraphs Satisfying CMSO Properties
    Mateus de Oliveira Oliveira
    Proc. of the 26th Annual Conference of the European Association for Computer Science Logic (CSL 2017).
    Stockholm, Sweden, August 2017

  • Representations of Monotone Boolean Functions by Linear Programs
    Mateus de Oliveira Oliveira, Pavel Pudlák
    Proc. of the 32nd Computational Complexity Conference (CCC 2017).
    Riga, Latvia, July 2017

  • Revisiting the Parameterized Complexity of Maximum-Duo Preservation String Mapping Problem.
    Christian Komusiewicz, Mateus de Oliveira Oliveira and Meirav Zehavi
    Proc. of the 28th Annual Symposium on Combinatorial Pattern Matching (CPM 2017)
    Warsaw, Poland, July 2017

2016

2015

Earlier

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