{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:43Z","timestamp":1725456223715},"publisher-location":"Berlin\/Heidelberg","reference-count":14,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012842","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"344-357","source":"Crossref","is-referenced-by-count":2,"title":["A decision procedure for unquantified formulas of graph theory"],"prefix":"10.1007","author":[{"given":"Louise E.","family":"Moser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1002\/cpa.3160330503","volume":"33","author":"A. Ferro","year":"1980","unstructured":"A. Ferro, E. G. Omodeo, and J. T. Schwartz, \u201cDecision procedures for elementary sublanguages of set theory. I. Multilevel syllogistic and some extensions,\u201d Comm. Pure App. Math. 33 (1980), pp. 599\u2013608.","journal-title":"Comm. Pure App. Math."},{"key":"23_CR2","first-page":"88","volume-title":"Proc. 5th Conf. on Automated Deduction","author":"A. Ferro","year":"1980","unstructured":"A. Ferro, E. G. Omodeo, and J. T. Schwartz, \u201cDecision procedures for some fragments of set theory,\u201d in: Proc. 5th Conf. on Automated Deduction, LNCS 87, (Springer-Verlag, Berlin-Heidelberg-New York, 1980), pp. 88\u201396."},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J. Hsiang","year":"1985","unstructured":"J. Hsiang, \u201cTopics in automated theorem proving and program generation,\u201d Artificial Intelligence 25 (1985), pp. 255\u2013300.","journal-title":"Artificial Intelligence"},{"issue":"3","key":"23_CR4","doi-asserted-by":"crossref","first-page":"61","DOI":"10.2307\/2268172","volume":"8","author":"J. C. C. McKinsey","year":"1943","unstructured":"J. C. C. McKinsey, \u201cThe decision problem for some classes of sentences without quantifiers,\u201d J. Symb. Logic 8, 3 (1943), pp. 61\u201376.","journal-title":"J. Symb. Logic"},{"key":"23_CR5","unstructured":"L. E. Moser, \u201cDecidability of formulas in graph theory,\u201d conditionally accepted by Fundamenta Informaticae."},{"issue":"2","key":"23_CR6","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen, \u201cSimplification by cooperating decision procedures,\u201d ACM Trans. Prog. Lang. and Syst. 1, 2 (1979), pp. 245\u2013257.","journal-title":"ACM Trans. Prog. Lang. and Syst."},{"issue":"2","key":"23_CR7","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. C. Oppen, \u201cFast decision procedures based on congruence closure,\u201d J. ACM 27, 2 (1980), pp. 356\u2013364.","journal-title":"J. ACM"},{"key":"23_CR8","first-page":"27","volume-title":"Proc. AMS SIAM Symp. Appl. Math.","author":"M. O. Rabin","year":"1973","unstructured":"M. O. Rabin and M. J. Fisher, \u201cSuper-exponential complexity of theorem proving procedures,\u201d in: Proc. AMS SIAM Symp. Appl. Math., (AMS, Providence, RI, 1973), pp. 27\u201342."},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(84)90021-5","volume":"32","author":"J. C. Raoult","year":"1984","unstructured":"J. C. Raoult, \u201cOn graph rewritings,\u201d Theor. Comp. Sci. 32 (1984), pp. 1\u201324.","journal-title":"Theor. Comp. Sci."},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson, \u201cA machine oriented logic based on the resolution principle,\u201d J. ACM 12 (1965), pp. 23\u201341.","journal-title":"J. ACM"},{"issue":"7","key":"23_CR11","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. E. Shostak","year":"1978","unstructured":"R. E. Shostak, \u201cAn algorithm for reasoning about equality,\u201d Comm. ACM, 21, 7 (1978), pp. 583\u2013585.","journal-title":"Comm. ACM"},{"issue":"1","key":"23_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"R. E. Shostak, \u201cDeciding combinations of theories,\u201d J. ACM 31, 1 (1984), pp. 1\u201312.","journal-title":"J. ACM"},{"key":"23_CR13","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/BFb0000050","volume-title":"Proc. 6th Conf. on Automated Deduction","author":"R. E. Shostak","year":"1982","unstructured":"R. E. Shostak, R. Schwartz, and P. M. Melliar-Smith, \u201cSTP: A mechanized logic for specification and verification,\u201d in: Proc. 6th Conf. on Automated Deduction, LNCS 138, (Springer-Verlag, Berlin-Heidelberg-New York, 1982), pp. 32\u201349."},{"issue":"2","key":"23_CR14","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"R. E. Tarjan","year":"1975","unstructured":"R. E. Tarjan, \u201cEfficiency of a good but not linear set union algorithm,\u201d J. ACM 22, 2 (1975), pp. 215\u2013225.","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012842.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:41Z","timestamp":1607353601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012842"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0012842","relation":{},"subject":[]}}