Abstract
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,\omega )\), where \(t_1 =t_2\) is an equation, and \(\omega \) 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 b that restricts the way in which variables are substituted for terms. We say that a proof is b-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,\omega )\) 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)\cdot |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 \(\omega \) such that \((t_1 =t_2,\omega )\) has a b-bounded proof, of depth d and width c, in time \(f(E,d,c,b)\cdot |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 \(\omega \) 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM (JACM) 41, 236–276 (1994)
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Resolution of Equations in Algebraic Structures, Rewriting Techniques, vol. 2, pp. 1–30. Academic Press (1989)
Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Inf. Comput. 121(2), 172–192 (1995)
Buss, S., Impagliazzo, R., Krajíček, J., Pudlák, P., Razborov, A.A., Sgall, J.: Proof complexity in algebraic systems and bounded depth frege systems with modular counting. Comp. Complex. 6(3), 256–298 (1996)
de Oliveira Oliveira, M.: Reachability in graph transformation systems and slice languages. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 121–137. Springer, Cham (2015). doi:10.1007/978-3-319-21145-9_8
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1. Equations and Initial Semantics. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (1985). doi:10.1007/978-3-642-69962-7
Freese, R.: Free modular lattices. Trans. Am. Math. Soc. 261, 81–91 (1980)
Goguen, J.A., Lin, K.: Specifying, programming and verifying with equational logic. In: We Will Show Them!, vol. 2, pp. 1–38. College Publications (2005)
Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs, 1st edn. MIT, Cambridge (1996)
Hillenbrand, T., Buch, A., Vogt, R., Löchner, B.: Waldmeister-high-performance equational deduction. J. Autom. Reas. 18(2), 265–270 (1997)
Hrubes, P., Tzameret, I.: The proof complexity of polynomial identities. In: 24th Conference on Computational Complexity, pp. 41–51 (2009)
Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed) Comput. Probl. Abstr. Algebra, 263–297 (1970)
Matijasevic, J.V.: Simple examples of undecidable associative calculi. Sov. Math. (Dokladi) 8(2), 555–557 (1967)
McCune, W.: Solution of the Robbins problem. J. Autom. Reas. 19(3), 263–276 (1997)
Meinke, K., Tucker, J.V.: Universal algebra. In: Handbook of Logic in Computer Science, Vol 1, pp. 189–409. Oxford University Press (1992)
Pigozzi, D.: Equational logic and equational theories of algebras, Technical report. Purdue University (1975)
Plaisted, D.A., Zhu, Y.: Equational reasoning using AC constraints. In: IJCAI, pp. 108–113. Morgan Kaufmann (1997)
Wampler-Doty, M.: A complete proof of the Robbins conjecture. Archive of Formal Proofs (2010)
Wechler, W.: Universal Algebra for Computer Scientists. Springer, Berlin (1992)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
de Oliveira Oliveira, M. (2017). Parameterized Provability in Equational Logic. In: Schmidt, R., Nalon, C. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2017. Lecture Notes in Computer Science(), vol 10501. Springer, Cham. https://doi.org/10.1007/978-3-319-66902-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-66902-1_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66901-4
Online ISBN: 978-3-319-66902-1
eBook Packages: Computer ScienceComputer Science (R0)