{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:32:42Z","timestamp":1743021162299,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319669014"},{"type":"electronic","value":"9783319669021"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66902-1_22","type":"book-chapter","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T11:34:20Z","timestamp":1504006460000},"page":"364-380","source":"Crossref","is-referenced-by-count":0,"title":["Parameterized Provability in Equational Logic"],"prefix":"10.1007","author":[{"given":"Mateus","family":"de Oliveira Oliveira","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,30]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM (JACM) 41, 236\u2013276 (1994)","journal-title":"J. ACM (JACM)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Resolution of Equations in Algebraic Structures, Rewriting Techniques, vol. 2, pp. 1\u201330. Academic Press (1989)","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"issue":"2","key":"22_CR3","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Inf. Comput. 121(2), 172\u2013192 (1995)","journal-title":"Inf. Comput."},{"issue":"3","key":"22_CR4","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/BF01294258","volume":"6","author":"S Buss","year":"1996","unstructured":"Buss, S., Impagliazzo, R., Kraj\u00ed\u010dek, J., Pudl\u00e1k, P., Razborov, A.A., Sgall, J.: Proof complexity in algebraic systems and bounded depth frege systems with modular counting. Comp. Complex. 6(3), 256\u2013298 (1996)","journal-title":"Comp. Complex."},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-21145-9_8","volume-title":"Graph Transformation","author":"M Oliveira Oliveira de","year":"2015","unstructured":"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\u2013137. Springer, Cham (2015). doi: 10.1007\/978-3-319-21145-9_8"},{"key":"22_CR6","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1. Equations and Initial Semantics","author":"H Ehrig","year":"1985","unstructured":"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"},{"key":"22_CR7","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1090\/S0002-9947-1980-0576864-X","volume":"261","author":"R Freese","year":"1980","unstructured":"Freese, R.: Free modular lattices. Trans. Am. Math. Soc. 261, 81\u201391 (1980)","journal-title":"Trans. Am. Math. Soc."},{"key":"22_CR8","unstructured":"Goguen, J.A., Lin, K.: Specifying, programming and verifying with equational logic. In: We Will Show Them!, vol. 2, pp. 1\u201338. College Publications (2005)"},{"key":"22_CR9","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1188.001.0001","volume-title":"Algebraic Semantics of Imperative Programs","author":"JA Goguen","year":"1996","unstructured":"Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs, 1st edn. MIT, Cambridge (1996)","edition":"1"},{"issue":"2","key":"22_CR10","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T Hillenbrand","year":"1997","unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: Waldmeister-high-performance equational deduction. J. Autom. Reas. 18(2), 265\u2013270 (1997)","journal-title":"J. Autom. Reas."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Hrubes, P., Tzameret, I.: The proof complexity of polynomial identities. In: 24th Conference on Computational Complexity, pp. 41\u201351 (2009)","DOI":"10.1109\/CCC.2009.9"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed) Comput. Probl. Abstr. Algebra, 263\u2013297 (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"2","key":"22_CR13","first-page":"555","volume":"8","author":"JV Matijasevic","year":"1967","unstructured":"Matijasevic, J.V.: Simple examples of undecidable associative calculi. Sov. Math. (Dokladi) 8(2), 555\u2013557 (1967)","journal-title":"Sov. Math. (Dokladi)"},{"issue":"3","key":"22_CR14","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. J. Autom. Reas. 19(3), 263\u2013276 (1997)","journal-title":"J. Autom. Reas."},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Meinke, K., Tucker, J.V.: Universal algebra. In: Handbook of Logic in Computer Science, Vol 1, pp. 189\u2013409. Oxford University Press (1992)","DOI":"10.1093\/oso\/9780198537359.003.0003"},{"key":"22_CR16","unstructured":"Pigozzi, D.: Equational logic and equational theories of algebras, Technical report. Purdue University (1975)"},{"key":"22_CR17","unstructured":"Plaisted, D.A., Zhu, Y.: Equational reasoning using AC constraints. In: IJCAI, pp. 108\u2013113. Morgan Kaufmann (1997)"},{"key":"22_CR18","unstructured":"Wampler-Doty, M.: A complete proof of the Robbins conjecture. Archive of Formal Proofs (2010)"},{"key":"22_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-76771-5","volume-title":"Universal Algebra for Computer Scientists","author":"W Wechler","year":"1992","unstructured":"Wechler, W.: Universal Algebra for Computer Scientists. Springer, Berlin (1992)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66902-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,26]],"date-time":"2024-06-26T14:48:43Z","timestamp":1719413323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66902-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319669014","9783319669021"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66902-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}