Project Publications

Preprints

Publications in Conferences and Journals

 
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

  • 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

  • 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)
  • 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 dos Santos Souza
    46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

2020

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

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