Parameterized Provability in Equational Logic

摘要

In this work we study the validity problem in equational logic from the perspective of parameterized complexity theory. We introduce a variant of equational logic in which sentences are pairs of the form (t_1 = t_2, ω), where t_1 = t_2 is an equation, and ω is an arbitrary ordering of the positions corresponding to subterms of t_1 and t_2- We call such pairs ordered equations. With each ordered equation, one may naturally associate a notion of width, and with each proof of validity of an ordered equation, one may naturally associate a notion of depth. We define the width of such a proof as the maximum width of an ordered equation occurring in it. Finally, we introduce a parameter 6 that restricts the way in which variables are substituted for terms. We say that a proof is 6-bounded if all substitutions used in it satisfy such restriction. Our main result states that the problem of determining whether an ordered equation (t_1 = t_2,w) has a b-bounded proof of depth d and width c, from a set of axioms E, can be solved in time f(E,d,c,b) • |t_1 =t_2|. In other words, this task is fixed parameter linear with respect to the depth, width and bound of the proof. Subsequently, we show that given a classical equation t_1 = t_2, one may determine whether there exists an ordering ω such that (t_1 = t_2,ω) has a b-bounded proof, of depth d and width c, in time f(E,d,c,b) • |t_1 = t_2|~(O(c)). In other words this task is fixed parameter tractable with respect to the depth and bound of the proof, and is in polynomial time for constant values of width. This second result is particularly interesting because the ordering ω is not given a priori, and thus, we are indeed parameterizing the provability of equations in classical equational logic. In view of the expressiveness of equational logic, our results give new fixed parameter tractable algorithms for a whole spectrum of problems, such as polynomial identity testing, program verification, automated theorem proving and the validity problem in undecidable equational theories.