Mateus de Oliveira Oliveira
Presentation
- I’m a Senior Lecturer at Stockholm University’s Department of Computer and System Sciences (Sweden).
- I also hold a part-time position as Associate Professor at the University of Bergen (Norway).
- I’m currently leading two research projects. SYMBOALGO is a 12 Million NOK project in the field of symbolic algorithms. AUTOPROVING is a 8 Million NOK project in the field of automated reasoning.
- 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.
Contact
- oliveira@dsv.su.se
Grants
- 2021-2025 – SYMBOALGO – Symbolic Algorithms: A Parameterized Approach. Research Council of Norway, FRIPRO, Ground-Breaking Research program (12 Million NOK).
- 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.
Research Team
- Boris Djalal – Researcher (2022-Present) – University of Bergen. Boris working in my project SYMBOALGO. Boris is working with proof formalization.
- Wim van den Broeck – Ph.D. Student (2022-Present) – University of Bergen. Wim is working in my project SYMBOALGO. I’m Wim’s main supervisor.
- Farhad Vadiee – Ph.D. Student (2019-Present)- University of Bergen. Farhad is working in my project AUTOPROVING. I’m Farhad main supervisor.
- Magnus Hegdahl – Bachelor Student (2022-Present) – University of Bergen. Magnus is working as a research assistant in my project AUTOPROVING.
Past Students and Team Members
- Emmanuel Arrighi – Ph.D. Student (2019-2022) – University of Bergen. I was Emmanuel’s main supervisor. Emmanuel successfully defended his thesis on 25/May/2022.
Participation in Program Committees
IJCAI 2023 (Senior PC member), SEA 2023 (PC member), AAAI 2023 (PC member), IJCAI 2022 (PC member), IWOCA 2022 (PC member), LSFA 2022 (PC member), AAAI 2021 (PC member)
Preprints
- From Width-Based Model Checking to Width-Based Automated Theorem Proving
Mateus de Oliveira Oliveira and Farhad Vadiee
Publications
2023
- From Width-Based Model Checking to Width-Based Automated Theorem Proving
Mateus de Oliveira Oliveira and Farhad Vadiee
37th AAAI Conference on Artificial Intelligence (AAAI 2023). Accepted.
- Synchronization and Diversity of Solutions
Emmanuel Arrighi, Henning Fernau, Mateus de Oliveira Oliveira and Petra Wolf
37th AAAI Conference on Artificial Intelligence (AAAI 2023). Accepted.
2022
- 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
Artificial Intelligence, 303:103644. 2022.
obs: Conference version appeared at IJCAI 2020
- Computing the Zig–Zag Number of Directed Graphs
Mitre Dourado, Celina de Figueiredo, Alexsander Andrade de Melo, Mateus de Oliveira Oliveira, Uéverton dos Santos Souza.
Discrete Applied Mathematics, 312:86-105. 2022.
- Second Order Finite Automata
Alexsander Andrade de Melo and Mateus de Oliveira Oliveira.
Theory of Computing Systems (Accepted)
- Synthesis and Analysis of Petri Nets from Causal Specifications.
Mateus de Oliveira Oliveira.
34th International Conference on Computer Aided Verification (Accepted)
- Mortality and Edge-to-Edge Reachability are Decidable on Surfaces
Mateus de Oliveira Oliveira and Olga Tveretina
ACM International Conference on Hybrid Systems (HSCC 2022). Accepted.
- On the Satisfiability of Smooth Grid CSPs.
Vasily Alferov and Mateus de Oliveira Oliveira
20th Symposium on Experimental Algorithms (SEA 2022). Accepted.
- Learning from Positive and Negative Examples: Dichotomies and Parameterized Algorithms
Jonas Ling, Mateus de Oliveira Oliveira and Petra Wolf
33rd International Workshop on Combinatorial Algorithms (IWOCA 2022). Accepted.
2021
- On Supergraphs Satisfying CMSO Properties
Mateus de Oliveira Oliveira
Logical Methods in Computer Science (Accepted)
obs: conference version appeared at CSL 2017
- Succinct Certification of Monotone Circuits.
Mateus Rodrigues Alves, Mateus de Oliveira Oliveira, Janio Carlos Nascimento Silva and Uéverton dos Santos Souza.
Theoretical Computer Science. (Accepted)
obs: conference version appeared at COCOON 2020
- On the Complexity of Intersection Non-emptiness for Star-Free Language Classes.
Emmanuel Arrighi, Henning Fernau, Stefan Hoffmann, Markus Holzer, Ismael Jecker, Mateus De Oliveira Oliveira and Petra Wolf
41st Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)
- Unitary Branching Programs: Learnability and Lower Bounds
Fidel Andino, Maria Kokkou, Mateus de Oliveira Oliveira, Farhad Vadiee
38th International Conference on Machine Learning (ICML 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)
- Order Reconfiguration under Width Constraints
Emmanuel Arrighi, Henning Fernau, Mateus de Oliveira Oliveira, Petra Wolf
46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
- Co-degeneracy and co-treewidth: Using the complement to solve dense instances
Gabriel Duarte, Mateus De Oliveira Oliveira and Uéverton Souza
46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
- Three is Enough for Steiner Trees
Emmanuel Arrighi, Mateus de Oliveira Oliveira
19th Symposium on Experimental Algorithms (SEA 2021)
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)
- Symbolic Solutions for Symbolic Constraint Satisfaction Problems
Alexsander Andrade de Melo, Mateus de Oliveira Oliveira
17th International Conference on Principles of Knowledge Representation and Reasoning (KR2020)
- 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)
- 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)
- 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.
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
- Ground Reachability and Joinability in Linear Term Rewriting Systems are Fixed Parameter Tractable with Respect to Depth
Mateus de Oliveira Oliveira
Proc. of the 11th International Symposium on Parameterized and Exact Computation (IPEC 2016)
Aarhus, Denmark , August 2016 - Causality in Petri Nets is MSO Definable
Mateus de Oliveira Oliveira
Proc. of the 23rd Workshop on Logic, Language, Information and Computation (WoLLIC 2016)
Puebla, Mexico, August 2016 - Satisfiability via Smooth Pictures
Mateus de Oliveira Oliveira
Proc. of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016)
Bordeaux, France, July 2016 - Size-Treewidth Tradeoffs for Circuits Computing the Element Distinctness Function
Mateus de Oliveira Oliveira
Proc. of the 33rd International Symposium on Theoretical Aspects of Computer Science (STACS 2016).
Orleans, France, February 2016. - An Algorithmic Metatheorem for Directed Treewidth (arxiv)
Mateus de Oliveira Oliveira
Discrete Applied Mathematics, Vol. 204, Pages 49–76, 2016
2015
- MSO logic and the Partial Order Semantics of Place/Transition-Nets.
Mateus de Oliveira Oliveira
Proc. of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015).
Cali, Colombia, October 2015. - A Slice Theoretic Approach for Embedding Problems on Digraphs.
Mateus de Oliveira Oliveira
Proc. of the 41st International workshop on Graph-Theoretic Concepts in Computer Science (WG 2015).
Munich, Germany, June 2015. - On the Satisfiability of Quantum Circuits of Small Treewidth.
Mateus de Oliveira Oliveira
Proc. of the 10th International Computer Science Symposium in Russia (CSR 2015).
Irkutsk, Russia, July 2015. - Reachability in Graph Transformation Systems and Slice Languages.
Mateus de Oliveira Oliveira
Proc. of the 8th International Conference on Graph Transformations (ICGT 2015).
L’Aquila, Italy, July 2015.
Earlier
- Subgraphs Satisfying MSO Properties on z-Topologically Orderable Digraphs
Mateus de Oliveira Oliveira
Proc. of the 8th International Symposium on Parameterized and Exact Computation (IPEC 2013)
Sophia Antipolis, France, September, 2013.
Excelent Student Paper Award at IPEC 2013. - Canonizable Partial Order Generators
Mateus de Oliveira Oliveira
Proc. of the 6th International Conference on Language and Automata Theory and Applications (LATA 2012)
A Coruña, Spain, March 2012. - Hasse diagram Generators and Petri Nets
Mateus de Oliveira Oliveira
Journal version: Fundamenta Informaticae 105(3):263-289, 2010.
Conference version: Proc. of the 30th Int. Conf. on Applications and Theory of Petri Nets (Petri Nets 2009).
Paris, France, June 2009.
Notes
- Embezzlement States are Universal for Non-Local Strategies
Mateus de Oliveira Oliveira
Doctoral Thesis
- Combinatorial Slice Theory
Mateus de Oliveira Oliveira
Teaching
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.