Project Publications


Publications in Conferences and Journals


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


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

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

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