Research map / Learning theory and algorithms / Combinatorial and search optimization

Sound Over-Approximation of Equational Reasoning with Variable-Preserving Rules Parameterized by Derivation Depth

AAAI 2025 · Learning theory and algorithms › Combinatorial and search optimization · approach: Logic and answer set programming theory · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Shows that ground equational reasoning with variable-preserving axioms can be soundly over-approximated in FPT time parameterized by derivation depth, via tree-automata completion.

Problem

Deciding whether a ground equation follows from a set of equational axioms is undecidable in general and NEXP-complete for depth bounded in binary; the paper targets tractable handling of bounded-depth parallel equational derivations.

Approach

Builds a tree automaton A(E,d,t) by iteratively applying a tree-automata completion step N(A,E) for each depth level, whose language soundly over-approximates terms reachable from t in d parallel rewriting steps; membership of t' in this language gives a YES/NO decision that is sound with respect to the equational closure.

Key results

• Main theorem: for fixed variable-preserving E, the algorithm decides YES for all equations derivable in depth at most d and NO for equations outside the equational closure, running in time f_E(d)·|t|·|t'|.
• Observation 7: for commutativity x+y=y+x, exponentially many terms are reachable in one parallel step while sequential derivations need Omega(n) steps.
• Theorem 8: a set of O(|Sigma|·r!) variable-preserving equations captures tree isomorphism in depth 1.

Surprising findings

• Parallel depth-1 derivations can be unboundedly more powerful than sequential derivations, reaching exponentially many terms in one step.

Limitations

• Full correctness analysis of automaton construction time deferred to a full version not included here.
• Over-approximation means YES may cover equations requiring derivations deeper than d.
• Result applies only to variable-preserving equations; general equations are undecidable.

Experimental setup

Builds on: Birkhoff's theorem tree automata completion multi-step rewriting (van Oostrom)

Closest papers by meaning

• On Learning Verifiers and Implications to Chain-of-Thought Reasoning (NeurIPS 2025 · similarity 0.83)
• Minimal Change in Modal Logic S5 (AAAI 2025 · similarity 0.83)
• HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs (ICML 2026 · similarity 0.83)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.83)
• An Algebraic Notion of Conditional Independence, and Its Application to Knowledge Representation (AAAI 2025 · similarity 0.83)
• DAG-Math: Graph-Guided Mathematical Reasoning in LLMs (ICLR 2026 · similarity 0.83)