4 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…