{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T21:55:27Z","timestamp":1777067727035,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540676645","type":"print"},{"value":"9783540451013","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_34","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"433-448","source":"Crossref","is-referenced-by-count":12,"title":["A Resolution Decision Procedure for Fluted Logic"],"prefix":"10.1007","author":[{"given":"Renate A.","family":"Schmidt","sequence":"first","affiliation":[]},{"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"34_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. J. Logic Computat.\u00a04(3), 217\u2013247 (1994)","journal-title":"J. Logic Computat."},{"key":"34_CR2","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2000","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L. Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 83\u201396. Springer, Heidelberg (1993)"},{"key":"34_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0054260","volume-title":"Automated Deduction - CADE-15","author":"H. Nivelle de","year":"1998","unstructured":"de Nivelle, H.: A resolution decision procedure for the guarded fragment. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 191\u2013204. Springer, Heidelberg (1998)"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56732-1","volume-title":"Resolution Methods for the Decision Problem","author":"C. Ferm\u00fcller","year":"1993","unstructured":"Ferm\u00fcller, C., Leitsch, A., Tammet, T., Zamov, N.: Resolution Methods for the Decision Problem. LNCS, vol.\u00a0679. Springer, Heidelberg (1993)"},{"key":"34_CR6","volume-title":"Handbook of Automated Reasoning","author":"C.G. Ferm\u00fcller","year":"2000","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)"},{"key":"34_CR7","first-page":"295","volume-title":"Fourteenth Annual IEEE Symposium on Logic in Computer Science","author":"H. Ganzinger","year":"1999","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Fourteenth Annual IEEE Symposium on Logic in Computer Science, pp. 295\u2013303. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"34_CR8","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/978-1-4613-0609-2_21","volume-title":"Mathematical Logic: Proceedings of the 1988 Heyting Summerschool","author":"G. Gargov","year":"1990","unstructured":"Gargov, G., Passy, S.: A note on Boolean modal logic. In: Petkov, P.P. (ed.) Mathematical Logic: Proceedings of the 1988 Heyting Summerschool, pp. 299\u2013309. Plenum Press, New York (1990)"},{"issue":"1","key":"34_CR9","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1093\/logcom\/2.1.5","volume":"2","author":"V. Goranko","year":"1992","unstructured":"Goranko, V., Passy, S.: Using the universal modality: Gains and questions. J. Logic Computat.\u00a02(1), 5\u201330 (1992)","journal-title":"J. Logic Computat."},{"key":"34_CR10","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J.Y. Halpern","year":"1992","unstructured":"Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence\u00a054, 319\u2013379 (1992)","journal-title":"Artificial Intelligence"},{"key":"34_CR11","unstructured":"Herzig, A.: A new decidable fragment of first order logic. In: Abstracts of the Third Logical Biennial, Summer School & Conference in Honour of S. C. Kleene, Varna, Bulgaria (1990)"},{"issue":"3","key":"34_CR12","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1305\/ndjfl\/1093870378","volume":"24","author":"I.L. Humberstone","year":"1983","unstructured":"Humberstone, I.L.: Inaccessible worlds. Notre Dame J. Formal Logic\u00a024(3), 346\u2013352 (1983)","journal-title":"Notre Dame J. Formal Logic"},{"issue":"2","key":"34_CR13","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1305\/ndjfl\/1093636937","volume":"28","author":"I.L. Humberstone","year":"1987","unstructured":"Humberstone, I.L.: The modal logic of \u2018all and only\u2019. Notre Dame J. Formal Logic\u00a028(2), 177\u2013188 (1987)","journal-title":"Notre Dame J. Formal Logic"},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"Hustadt, U., Schmidt, R.A.: An empirical analysis of modal theorem provers. J. Appl. Non-Classical Logics\u00a09(4) (1999)","DOI":"10.1080\/11663081.1999.10510981"},{"key":"34_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48660-7_12","volume-title":"Automated Deduction - CADE-16","author":"U. Hustadt","year":"1999","unstructured":"Hustadt, U., Schmidt, R.A.: Maslov\u2019s class K revisited. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 172\u2013186. Springer, Heidelberg (1999)"},{"key":"34_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-46508-1_13","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: Issues of decidability for description logics in the framework of resolution. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 192\u2013206. Springer, Heidelberg (2000)"},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Hustadt, U., Schmidt, R.A.: A resolution decision procedure for fluted logic. Technical Report UMCS-00-3-1, University of Manchester, UK (2000)","DOI":"10.1007\/10721959_34"},{"issue":"3","key":"34_CR18","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner Jr.","year":"1976","unstructured":"Joyner Jr., W.H.: Resolution strategies as decision procedures. J. ACM\u00a023(3), 398\u2013417 (1976)","journal-title":"J. ACM"},{"issue":"5","key":"34_CR19","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1093\/logcom\/7.5.581","volume":"7","author":"H.J. Ohlbach","year":"1997","unstructured":"Ohlbach, H.J., Schmidt, R.A.: Functional translation and second-order frame properties of modal logics. J. Logic Computat.\u00a07(5), 581\u2013603 (1997)","journal-title":"J. Logic Computat."},{"key":"34_CR20","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Computat.\u00a02, 293\u2013304 (1986)","journal-title":"J. Symbolic Computat."},{"issue":"1","key":"34_CR21","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1305\/ndjfl\/1040067318","volume":"37","author":"W.C. Purdy","year":"1996","unstructured":"Purdy, W.C.: Decidability of fluted logic with identity. Notre Dame J. Formal Logic\u00a037(1), 84\u2013104 (1996)","journal-title":"Notre Dame J. Formal Logic"},{"issue":"2","key":"34_CR22","doi-asserted-by":"publisher","first-page":"608","DOI":"10.2307\/2275678","volume":"61","author":"W.C. Purdy","year":"1996","unstructured":"Purdy, W.C.: Fluted formulas and the limits of decidability. J. Symbolic Logic\u00a061(2), 608\u2013620 (1996)","journal-title":"J. Symbolic Logic"},{"key":"34_CR23","unstructured":"Purdy, W.C.: Surrogate variables in natural language. In: B\u00f6ttner, M. (ed.) Proc. of the Workshop on Variable-Free Semantics (1996) (to appear)"},{"key":"34_CR24","doi-asserted-by":"publisher","first-page":"1439","DOI":"10.2307\/2586789","volume":"64","author":"W.C. Purdy","year":"1999","unstructured":"Purdy, W.C.: Quine\u2019s \u2018limits of decision\u2019. J. Symbolic Logic\u00a064, 1439\u20131466 (1999)","journal-title":"J. Symbolic Logic"},{"key":"34_CR25","unstructured":"Quine, W.V.: Variables explained away. In: Proc. American Philosophy Society, vol.\u00a0104, pp. 343\u2013347 (1960)"},{"issue":"4","key":"34_CR26","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1023\/A:1006043519663","volume":"22","author":"R.A. Schmidt","year":"1999","unstructured":"Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Automated Reasoning\u00a022(4), 379\u2013396 (1999)","journal-title":"J. Automated Reasoning"},{"key":"34_CR27","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivations in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, pp. 115\u2013125, Consultants Bureau, New York (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"34_CR28","unstructured":"Weidenbach, C.: SPASS (1999), http:\/\/spass.mpi-sb.mpg.de"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T19:01:50Z","timestamp":1736708510000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/10721959_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}