{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:31:37Z","timestamp":1740547897257,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223450"},{"type":"electronic","value":"9783540259848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25984-8_10","type":"book-chapter","created":{"date-parts":[[2010,9,11]],"date-time":"2010-09-11T02:31:38Z","timestamp":1284172298000},"page":"168-182","source":"Crossref","is-referenced-by-count":7,"title":["Modular Proof Systems for Partial Functions with Weak Equality"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[]},{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"10_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM\u00a045(6) (1998)","DOI":"10.1145\/293347.293352"},{"issue":"3\/4","key":"10_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing\u00a05(3\/4), 193\u2013212 (1994)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"10_CR4","series-title":"Mathematical Research","doi-asserted-by":"crossref","DOI":"10.1515\/9783112720875","volume-title":"A Model Theoretic Oriented Approach to Partial Algebras: Introduction to Theory and Application of Partial Algebras, Part I","author":"P. Burmeister","year":"1986","unstructured":"Burmeister, P.: A Model Theoretic Oriented Approach to Partial Algebras: Introduction to Theory and Application of Partial Algebras, Part I. Mathematical Research, vol.\u00a031. Akademie-Verlag, Berlin (1986)"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1002\/malq.19950410204","volume":"41","author":"S. Burris","year":"1995","unstructured":"Burris, S.: Polynomial time uniform word problems. Mathematical Logic Quarterly\u00a041, 173\u2013182 (1995)","journal-title":"Mathematical Logic Quarterly"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1112\/jlms\/s1-28.1.76","volume":"28","author":"T. Evans","year":"1953","unstructured":"Evans, T.: Embeddability and the word problem. J. London Math. Soc.\u00a028, 76\u201380 (1953)","journal-title":"J. London Math. Soc."},{"key":"10_CR7","first-page":"81","volume-title":"Sixteenth Annual IEEE Symposium on Logic in Computer Science","author":"H. Ganzinger","year":"2001","unstructured":"Ganzinger, H.: Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In: Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp. 81\u201392. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Ghilardi, S.: Quantifier elimination and provers integration. Electronic Notes in Theoretical Computer Science\u00a086(1) (2003)","DOI":"10.1016\/S1571-0661(04)80650-9"},{"key":"10_CR9","volume-title":"Universal algebra","author":"G. Gr\u00e4tzer","year":"1968","unstructured":"Gr\u00e4tzer, G.: Universal algebra, 2nd edn. Springer, Heidelberg (1968)","edition":"2"},{"key":"10_CR10","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/3-540-58156-1_26","volume-title":"Automated Deduction - CADE-12","author":"M. Kerber","year":"1994","unstructured":"Kerber, M., Kohlhase, M.: A mechanization of strong Kleene logic for partial functions. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 371\u2013385. Springer, Heidelberg (1994)"},{"key":"10_CR11","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. D. Van Nostrand Company, Inc., Princeton (1952)"},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"10_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1022587501759","volume":"30","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. Journal of Automated Reasoning\u00a030(1), 1\u201331 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR14","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems, First International Workshop, Munich, Germany","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, First International Workshop, Munich, Germany. Applied Logic Series, vol.\u00a03, pp. 103\u2013119. Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.: Combining non-stably infinite theories. Electronic Notes in Theoretical Computer Science\u00a086(1) (2003)","DOI":"10.1016\/S1571-0661(04)80651-0"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25984-8_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T18:10:01Z","timestamp":1740507001000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25984-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223450","9783540259848"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25984-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}