{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:02Z","timestamp":1761611102240},"reference-count":31,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3850,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[2003,1]]},"DOI":"10.1016\/s0747-7171(02)00092-5","type":"journal-article","created":{"date-parts":[[2003,1,17]],"date-time":"2003-01-17T18:39:55Z","timestamp":1042828795000},"page":"21-58","source":"Crossref","is-referenced-by-count":15,"title":["Deciding the guarded fragments by resolution"],"prefix":"10.1016","volume":"35","author":[{"given":"Hans de","family":"Nivelle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maarten de","family":"Rijke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(02)00092-5_B1","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1023\/A:1004275029985","article-title":"Modal languages and bounded fragments of predicate logic","volume":"27","author":"Andr\u00e9ka","year":"1998","journal-title":"J. Phil. Logic"},{"key":"10.1016\/S0747-7171(02)00092-5_B2","doi-asserted-by":"crossref","unstructured":"Areces, C., 2000. Logic Engineering, Ph.D. Thesis. ILLC, University of Amsterdam","DOI":"10.1093\/jigpal\/8.5.653"},{"key":"10.1016\/S0747-7171(02)00092-5_B3","doi-asserted-by":"crossref","unstructured":"Baaz, M., Ferm\u00fcller, C., Leitsch, A., 1994. A non-elementary speed up in proof length by structural clause form transformation. Proceedings LICS\u201994. pp. 213\u2013219","DOI":"10.1109\/LICS.1994.316070"},{"key":"10.1016\/S0747-7171(02)00092-5_B4","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0747-7171(02)00092-5_B5","unstructured":"Boyer, R., 1971. Locking: A Restriction of Resolution, Ph.D. Thesis. University of Texas at Austin"},{"key":"10.1016\/S0747-7171(02)00092-5_B6","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/S0747-7171(02)00092-5_B7","doi-asserted-by":"crossref","unstructured":"de Nivelle, H., 1993. Generic resolution in propositional modal systems. LPAR\u201993. LNAI, vol. 698. pp. 241\u2013252","DOI":"10.1007\/3-540-56944-8_57"},{"key":"10.1016\/S0747-7171(02)00092-5_B8","doi-asserted-by":"crossref","unstructured":"de Nivelle, H., 1994. Resolution games and non-liftable resolution orderings. CSL\u201994. pp. 279\u2013293","DOI":"10.1007\/BFb0022263"},{"key":"10.1016\/S0747-7171(02)00092-5_B9","doi-asserted-by":"crossref","unstructured":"de Nivelle, H., 1998. A resolution decision procedure for the guarded fragment. CADE\u201998. pp. 191\u2013204","DOI":"10.1007\/BFb0054260"},{"key":"10.1016\/S0747-7171(02)00092-5_B10","unstructured":"de Nivelle, H., 1999a. The Bliksem Theorem Prover. Can be obtained from: http:\/\/www.mpi-sb.mpg.de\/~bliksem"},{"key":"10.1016\/S0747-7171(02)00092-5_B11","unstructured":"de Nivelle, H., 1999b. Translation of S4 and K4 into the guarded fragment and the 2-variable fragment (manuscript)"},{"key":"10.1016\/S0747-7171(02)00092-5_B12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","article-title":"Modal resolution in clausal form","volume":"65","author":"Enjalbert","year":"1989","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/S0747-7171(02)00092-5_B13","volume":"vol. 679","author":"Ferm\u00fcller","year":"1993"},{"key":"10.1016\/S0747-7171(02)00092-5_B14","series-title":"Aspects of Philosophical Logic","first-page":"91","article-title":"Expressive functional completeness in tense logic","author":"Gabbay","year":"1981"},{"key":"10.1016\/S0747-7171(02)00092-5_B15","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., de Nivelle, H., 1999. A superposition decision procedure for the guarded fragment with equality. LICS\u201999. pp. 295\u2013303","DOI":"10.1109\/LICS.1999.782624"},{"key":"10.1016\/S0747-7171(02)00092-5_B16","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Meyer, C., Veanes, M., 1999. The two-variable guarded fragment with transitive relations. LICS\u201999, pp. 24\u201334","DOI":"10.1109\/LICS.1999.782582"},{"key":"10.1016\/S0747-7171(02)00092-5_B17","unstructured":"Gr\u00e4del, E., 1997. On the restraining power of guards. J. Symb. Log. (to appear)"},{"key":"10.1016\/S0747-7171(02)00092-5_B18","doi-asserted-by":"crossref","first-page":"53","DOI":"10.2307\/421196","article-title":"On the decision problem for two-variable first-order logic","volume":"3","author":"Gr\u00e4del","year":"1997","journal-title":"Bull. Symb. Logic"},{"key":"10.1016\/S0747-7171(02)00092-5_B19","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Walukiewicz, I., 1999. Guarded fixed point logic. LICS\u201999. Trento, pp. 45\u201354","DOI":"10.1109\/LICS.1999.782585"},{"key":"10.1016\/S0747-7171(02)00092-5_B20","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0890-5401(89)90055-2","article-title":"Definability with a bounded number of bound variables","volume":"83","author":"Immerman","year":"1989","journal-title":"Inf. Comput."},{"key":"10.1016\/S0747-7171(02)00092-5_B21","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/S0004-3702(98)00109-X","article-title":"Expressiveness of concept expressions in first-order description logics","volume":"107","author":"Kurtonina","year":"1999","journal-title":"Artif. Intell."},{"key":"10.1016\/S0747-7171(02)00092-5_B22","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","article-title":"The computational complexity of provability in systems of modal propositional logic","volume":"6","author":"Ladner","year":"1977","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0747-7171(02)00092-5_B23","series-title":"Texts in Theoretical Computer Science","article-title":"The resolution calculus","author":"Leitsch","year":"1997"},{"key":"10.1016\/S0747-7171(02)00092-5_B24","doi-asserted-by":"crossref","unstructured":"McCune, W., 1995. Otter 3.0 Reference Manual and Guide. Argonne National Laboratory, Mathematics and Computer Science Division. Available from: ftp.mcs.anl.gov, directory pub\/Otter","DOI":"10.2172\/10129052"},{"key":"10.1016\/S0747-7171(02)00092-5_B25","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1002\/malq.19750210118","article-title":"On languages with two variables","volume":"21","author":"Mortimer","year":"1975","journal-title":"Z. Math. Log. Grundl. Math."},{"key":"10.1016\/S0747-7171(02)00092-5_B26","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/BF00881919","article-title":"A note on assumptions about skolem functions","volume":"15","author":"Ohlbach","year":"1995","journal-title":"J. Autom. Reasoning"},{"key":"10.1016\/S0747-7171(02)00092-5_B27","unstructured":"Schmidt, R., 1997. Optimized Modal Translation and Resolution, Ph.D. Thesis. Max Planck Institut f\u00fcr Informatik, Saarbr\u00fccken"},{"key":"10.1016\/S0747-7171(02)00092-5_B28","doi-asserted-by":"crossref","unstructured":"Tammet, T., 1990. The resolution program, able to decide some solvable classes. Proceedings COLOG-88, pp. 300\u2013312","DOI":"10.1007\/3-540-52335-9_61"},{"key":"10.1016\/S0747-7171(02)00092-5_B29","unstructured":"van Benthem, J., 1997. Dynamic bits and pieces. Technical Report LP-97-01, ILLC. University of Amsterdam"},{"key":"10.1016\/S0747-7171(02)00092-5_B30","doi-asserted-by":"crossref","unstructured":"Vardi, M., 1997. Why is modal logic so robustly decidable? In: Immerman, N., Kolaitis, P. (Eds.), Descriptive Complexity and Finite Models. pp. 149\u2013183","DOI":"10.1090\/dimacs\/031\/05"},{"key":"10.1016\/S0747-7171(02)00092-5_B31","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., 1997. The Spass & Flotter Users Guide, Version 0.55. Available from: ftp.mpi-sb.mpg.de, directory pub\/SPASS","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717102000925?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717102000925?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,12]],"date-time":"2020-03-12T01:49:56Z","timestamp":1583977796000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717102000925"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,1]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,1]]}},"alternative-id":["S0747717102000925"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(02)00092-5","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[2003,1]]}}}