{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:43:41Z","timestamp":1749725021793,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054260","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"191-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["A resolution decision procedure for the guarded fragment"],"prefix":"10.1007","author":[{"given":"Hans","family":"de Nivelle","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"21_CR1","unstructured":"H. Andr\u00e9ka, J. van Benthem, I. N\u00e9meti, Modal Languages and Bounded Fragments of Predicate Logic, ILLC Research Report ML-96-03, 1996."},{"key":"21_CR2","unstructured":"M. Baaz, C. Ferm\u00fcller, A. Leitsch, A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation, In LICS 94."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Leitsch, On Skolemization and Proof Complexity, Fundamenta Informatica, Vol. 20\u20134, 1994.","DOI":"10.3233\/FI-1994-2044"},{"key":"21_CR4","volume-title":"Exploring Logical Dynamics","author":"J. van Benthem","year":"1996","unstructured":"J. van Benthem, Exploring Logical Dynamics, CSLI Publications, Stanford, California USA, 1996."},{"key":"21_CR5","unstructured":"J. van Benthem, Dynamic Bits and Pieces, LP-97-01, Research Report of the Institute for Logic, Language and Information, 1997."},{"key":"21_CR6","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1996","unstructured":"E. B\u00f6rger, E. Gr\u00c4del, Y. Gurevich, The Classical Decision Problem, Springer Verlag, Berlin Heidelberg, 1996."},{"key":"21_CR7","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/BF01880326","volume":"7","author":"L. Catach","year":"1991","unstructured":"L. Catach, TABLEAUX, a general theorem prover for modal logics, Journal of automated reasoning 7, pp. 489\u2013510, 1991.","journal-title":"Journal of automated reasoning"},{"key":"21_CR8","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C-L. Chang","year":"1973","unstructured":"C-L. Chang, R. C-T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"21_CR9","unstructured":"B. Dreben, W.D. Goldfarb, The Decision Problem, Solvable Classes of Quantificational Formulas, Addision-Wesley Publishing Company, Inc. 1979."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"P. Enjalbert, L. Fari\u00f1as del Cerro, Modal resolution in clausal form, Theoretical Computer Science 65, 1989.","DOI":"10.1016\/0304-3975(89)90137-0"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"L. Fari\u00f1as del Cerro and A. Herzig, linear modal deductions, CADE '88, pp. 487\u2013499, 1988.","DOI":"10.1007\/BFb0012851"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, N. Zamov, Resolution Methods for the Decision Problem, Lecture Notes in Artificial Intelligence 679, Springer Verlag, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"21_CR13","first-page":"191","volume":"4","author":"M. Fitting","year":"1991","unstructured":"M. Fitting, First-order modal tableaux, Journal of automated resoning 4, pp. 191\u2013213, 1991.","journal-title":"Journal of automated resoning"},{"key":"21_CR14","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1093\/logcom\/1.1.83","volume":"1","author":"M. Fitting","year":"1990","unstructured":"M. Fitting, Destructive Modal Resolution, Journal of Logic and Computation, volume 1, pp. 83\u201397, 1990.","journal-title":"Journal of Logic and Computation"},{"key":"21_CR15","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0743-1066(92)90028-2","volume":"12","author":"A. Foret","year":"1992","unstructured":"A. Foret, Rewrite rule systems for modal propositional logic, Journal of logic programming 12, pp. 281\u2013298, 1992.","journal-title":"Journal of logic programming"},{"key":"21_CR16","unstructured":"E. Gr\u00c4del, On the Restraining Power of Guards, manuscript, 1997."},{"issue":"1","key":"21_CR17","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W. H. Joyner","year":"1976","unstructured":"W. H. Joyner, Resolution Strategies as Decision Procedures, J. ACM 23, 1 (July 1976),1 pp. 398\u2013417, 1976.","journal-title":"J. ACM"},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R.E. Ladner","year":"1977","unstructured":"R.E. Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM Journal on Computing 6, pp 467\u2013480, 1977.","journal-title":"SIAM Journal on Computing"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"W. W. McCune, Otter 3.0 Reference Manual and Guide, Argonne National Laboratory, Mathematics and Computer Science Division, can be obtained from ftp.mcs.anl.gov, directory pub\/Otter, 1995.","DOI":"10.2172\/10129052"},{"key":"21_CR20","unstructured":"H. de Nivelle, Generic modal resolution, Technical Report 92-90, Delft University of Technology, fac. TWI, 1992."},{"key":"21_CR21","unstructured":"Generic Resolution in Propositional Modal Systems, in LPAR 93, Springer Verlag Berlin, 1993."},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Resolution Games and Non-Liftable Resolution Orderings, in CSL 94, pp. 279\u2013293, Springer Verlag, 1994.","DOI":"10.1007\/BFb0022263"},{"key":"21_CR23","unstructured":"H. de Nivelle, Ordering Refinements of Resolution, Ph. D. Thesis, Delft University of Technology, 1995."},{"key":"21_CR24","unstructured":"H. de Nivelle, Resolution Decides the Guarded Fragment, ILLC-Report CT-1998-01, 1998."},{"key":"21_CR25","unstructured":"H.J. Ohlbach, A resolution calculus for modal logics, PhD thesis, Universit\u00c4t Kaiserslautern, 1988."},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"H.J. Ohlbach, A resolution calculus for modal logics, CADE '88, pp. 500\u2013516, 1988.","DOI":"10.1007\/BFb0012852"},{"key":"21_CR27","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BF00881919","volume":"2","author":"H-J. Ohlbach","year":"1995","unstructured":"H-J. Ohlbach, C. Weidenbach, A note on Assumptions About Skolem Functions, Journal of Automated Reasoning 15, Vol. 2, pp. 267\u2013275, 1995.","journal-title":"Journal of Automated Reasoning 15"},{"key":"21_CR28","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson, A Machine Oriented Logic Based on the Resolution Principle, Journal of the ACM, Vol. 12. pp. 23\u201341, 1965","journal-title":"Journal of the ACM"},{"key":"21_CR29","unstructured":"The CADE-13 Automated Theorem Proving System Competition, Journal of Automated Reasoning Special Issue, Vol. 18, No. 2, Edited by G. Sutcliffe and C. Suttner, 1996."},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"T. Tammet, The Resolution Program, Able to Decide some Solvable Classes, in COLOG-88, Springer LNCS, pp. 300\u2013312, 1990.","DOI":"10.1007\/3-540-52335-9_61"},{"key":"21_CR31","unstructured":"C. Weidenbach, (Max-Planck-Institut f\u00fcr Informatik), The Spass & Flotter Users Guide, Version 0.55, can be obtained from ftp.mpi-sb.mpg.de, directory pub\/SPASS, 1997."},{"key":"21_CR32","first-page":"5","volume":"128","author":"N.K. Zamov","year":"1972","unstructured":"N.K. Zamov, On a Bound for the Complexity of Terms in the Resolution Method, Trudy Mat. Inst. Steklov 128, pp. 5\u201313, 1972.","journal-title":"Trudy Mat. Inst. Steklov"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054260","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T23:21:45Z","timestamp":1676676105000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054260"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/bfb0054260","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}