From Width-Based Model Checking to Width-Based Automated Theorem Proving
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 combinatorial properties on graphs. In this work, we introduce a general framework to convert a large class of width-based model-checking algorithms into algorithms that can be used to test the validity of graph-theoretic conjectures on classes of graphs of bounded width. Our framework is modular and can be applied with respect to several well-studied width measures for graphs, including treewidth and cliquewidth. As a quantitative application of our framework, we prove analytically that for several long-standing graph-theoretic conjectures, there exists an algorithm that takes a number $k$ as input and correctly determines in time double-exponential in $k^{O(1)}$ whether the conjecture is valid on all graphs of treewidth at most $k$. These upper bounds, which may be regarded as upper-bounds on the size of proofs/disproofs for these conjectures on the class of graphs of treewidth at most $k$, improve significantly on theoretical upper bounds obtained using previously available techniques.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingvalidSimilar Papers 제목 키워드 기반
Parameterized Complexity Of Representing Models Of MSO Formulas
Monadic second order logic (MSO2) plays an important role in parameterized complexity due to the Courcelle's theorem. This theorem states that the problem of checking if a given graph has a property specified by a given …
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving
We study methods for automated parsing of informal mathematical expressions into formal ones, a main prerequisite for deep computer understanding of informal mathematical texts. We propose a context-based parsing approac…
Automated Theorem ProvingSemantic ParsingCktFormalizer: Autoformalization of Natural Language into Circuit Representations
LLMs can generate hardware descriptions from natural language specifications, but the resulting Verilog often contains width mismatches, combinational loops, and incomplete case logic that pass syntax checks yet fail in …
Proceedings 6th International Workshop on Theorem proving components for Educational software
The 6th International Workshop on Theorem proving components for Educational software (ThEdu'17) was held in Gothenburg, Sweden, on 6 Aug 2017. It was associated to the conference CADE26. Topics of interest include: meth…
Automated Theorem ProvingA Numerical Investigation of the Minimum Width of a Neural Network
Neural network width and depth are fundamental aspects of network topology. Universal approximation theorems provide that with increasing width or depth, there exists a neural network that approximates a function arbitra…