{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:36Z","timestamp":1725557916480},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250517"},{"type":"electronic","value":"9783540322542"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32254-2_8","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T15:16:54Z","timestamp":1277219814000},"page":"132-138","source":"Crossref","is-referenced-by-count":0,"title":["Solving First-Order Constraints over the Monadic Class"],"prefix":"10.1007","author":[{"given":"Dimitri","family":"Chubarov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"ch. 10","first-page":"609","volume-title":"Handbook of Automated Reasoning","author":"A. Degtyarev","year":"2001","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 10, vol.\u00a0I, pp. 609\u2013704. Elsevier Science, Amsterdam (2001)"},{"key":"8_CR2","first-page":"338","volume-title":"Proc. IEEE Conference on Logic in Computer Science (LICS)","author":"J.H. Gallier","year":"1987","unstructured":"Gallier, J.H., Raatz, S., Snyder, W.: Theorem proving using rigid E-unification: Equational matings. In: Proc. IEEE Conference on Logic in Computer Science (LICS), pp. 338\u2013346. IEEE Computer Society Press, Los Alamitos (1987)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Gurevich, Y.: The decision problem for the logic of predicates and operations, vol.\u00a08, pp. 284\u2013308 (1969)","DOI":"10.1007\/BF02306690"},{"key":"8_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574","volume-title":"Model theory","author":"W. Hodges","year":"1993","unstructured":"Hodges, W.: Model theory. Cambridge University Press, Cambridge (1993)"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H. Lewis","year":"1980","unstructured":"Lewis, H.: Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences\u00a021, 317\u2013353 (1980)","journal-title":"Journal of Computer and System Sciences"},{"key":"8_CR6","first-page":"563","volume":"32","author":"M. L\u00f6b","year":"1967","unstructured":"L\u00f6b, M.: Decidability of the monadic predicate calculus with unary function symbols. Journal of Symbolic Logic\u00a032, 563 (1967)","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR7","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/BFb0064872","volume-title":"Logic Colloquium: Symposium on Logic Held at Boston","author":"A. Meyer","year":"1975","unstructured":"Meyer, A.: Weak monadic second order theory of successor is not elementaryrecursive. In: Parikh, R. (ed.) Logic Colloquium: Symposium on Logic Held at Boston. Lecture Notes in Mathematics, vol.\u00a0453, pp. 132\u2013154. Springer, Heidelberg (1975)"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society\u00a0141(1), 1\u201335 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/3-540-63385-5_52","volume-title":"Computational Logic and Proof Theory","author":"M. Veanes","year":"1997","unstructured":"Veanes, M.: The undecidability of simultaneous rigid E-unification with two variables. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol.\u00a01289, pp. 305\u2013318. Springer, Heidelberg (1997)"},{"key":"8_CR10","unstructured":"Voronkov, A.: Strategies in rigid-variable methods. In: Pollack, M.E. (ed.) Proc. of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI 1997), Nagoya, Japan, August 23-29, vol.\u00a01, pp. 114\u2013119 (1997)"},{"key":"8_CR11","first-page":"252","volume-title":"Proc. IEEE Conference on Logic in Computer Science (LICS)","author":"A. Voronkov","year":"1998","unstructured":"Voronkov, A.: Herbrand\u2019s theorem, automated reasoning and semantic tableaux. In: Proc. IEEE Conference on Logic in Computer Science (LICS), pp. 252\u2013263. IEEE Computer Society Press, Los Alamitos (1998)"},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"984","DOI":"10.2307\/2586615","volume":"64","author":"A. Voronkov","year":"1999","unstructured":"Voronkov, A.: The ground-negative fragment of first-order logic is $ II^p_2$ -complete. Journal of Symbolic Logic\u00a064(3), 984\u2013990 (1999)","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/S0304-3975(98)00317-X","volume":"224","author":"A. Voronkov","year":"1999","unstructured":"Voronkov, A.: Simultaneous rigid E-unification and other decision problems related to Herbrand\u2019s theorem. Theoretical Computer Science\u00a0224, 319\u2013352 (1999)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Mechanizing Mathematical Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32254-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T05:37:58Z","timestamp":1559194678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32254-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250517","9783540322542"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32254-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}