4 citations · 4 across the 12 of their papers we have counts for
12 papers
State Canonization and Early Pruning in Width-Based Automated Theorem Proving
Mateus de Oliveira Oliveira, Sam Urmian
Width-based automated theorem proving is a framework where counterexamples to graph-theoretic conjectures are searched width-wise relative to some graph width measure, such as tree…
From Width-Based Model Checking to Width-Based Automated Theorem Proving
Mateus de Oliveira Oliveira, Sam Urmian
In the field of parameterized complexity theory, the study of graph width measures has been intimately connected with the development of width-based model checking algorithms for c…
Second-Order Finite Automata
Alexsander Andrade de Melo, Mateus de Oliveira Oliveira
Traditionally, finite automata theory has been used as a framework for the representation of possibly infinite sets of strings. In this work, we introduce the notion of second-orde…
On the Width of Regular Classes of Finite Structures
Alexsander Andrade de Melo, Mateus de Oliveira Oliveira
In this work, we introduce the notion of decisional width of a finite relational structure and the notion of decisional width of a regular class of finite structures. Our main resu…
On Supergraphs Satisfying CMSO Properties
Mateus de Oliveira Oliveira
Let CMSO denote the counting monadic second order logic of graphs. We give a constructive proof that for some computable function , there is an algorithm that tak…
A Near-Quadratic Lower Bound for the Size of Quantum Circuits of Constant Treewidth
Mateus de Oliveira Oliveira
We show that any quantum circuit of treewidth , built from -qubit gates, requires at least gates to compute the element disti…
An Algorithmic Metatheorem for Directed Treewidth
Mateus de Oliveira Oliveira
The notion of directed treewidth was introduced by Johnson, Robertson, Seymour and Thomas [Journal of Combinatorial Theory, Series B, Vol 82, 2001] as a first step towards an algor…
On the Satisfiability of Quantum Circuits of Small Treewidth
Mateus de Oliveira Oliveira
It has been known for almost three decades that many -hard optimization problems can be solved in polynomial time when restricted to structures of constant treewidth.…
Automated Verification, Synthesis and Correction of Concurrent Systems via MSO Logic
Mateus de Oliveira Oliveira
In this work we provide algorithmic solutions to five fundamental problems concerning the verification, synthesis and correction of concurrent systems that can be modeled by bounde…
Subgraphs Satisfying MSO Properties on z-Topologically Orderable Digraphs
Mateus de Oliveira Oliveira
We introduce the notion of z-topological orderings for digraphs. We prove that given a digraph G on n vertices admitting a z-topological order- ing, together with such an ordering,…
Embezzlement States are Universal for Non-Local Strategies
Mateus de Oliveira Oliveira
We prove that the family of embezzlement states defined by van Dam and Hayden [vanDamHayden2002] is universal for both quantum and classical entangled two-prover non-local games wi…
Canonizable Partial Order Generators and Regular Slice Languages
Mateus de Oliveira Oliveira
In a previous work we introduced slice graphs as a way to specify both infinite languages of directed acyclic graphs (DAGs) and infinite languages of partial orders. Therein we foc…