A Conjecture for ATP Research

TL;DR

The paper addresses whether factorization of formulas with multiplicities in the Connection Method (CM) can match the efficiency and complexity advantages of resolution (RM). It analyzes a concrete example where factorization reduces a CM proof from $F_1^{\mu_1}$ to $F_1^{\mu_1'}$, producing a DAG and suggesting potential speedups in proof search. The central contribution is a conjecture: CM with factorization for formulas with multiplicities possesses the RM-like $C_c$ property, and any factorized CM proof can be linearly transformed to a resolution proof, and vice versa, with CSC interpretable through factorization. If validated, this could shift ATP toward CM as a primary proof method by achieving RM-like complexity and enabling new search strategies that exploit substructure sharing and multiplicity-aware factorization.

Abstract

This note generalizes factorization for formulas with multiplicities and conjectures that the connection method along with this feature is computationally as powerful as resolution, also seen from a complexity point of view.

Figures (1)

• Figure 1: A connection proof for formula $F_1^{\mu_1}$.