{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T17:09:58Z","timestamp":1659632998044},"reference-count":34,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"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":3791,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1016\/s0890-5401(03)00016-6","type":"journal-article","created":{"date-parts":[[2003,3,4]],"date-time":"2003-03-04T15:38:35Z","timestamp":1046792315000},"page":"99-130","source":"Crossref","is-referenced-by-count":1,"title":["Extracting models from clause sets saturated under semantic refinements of the resolution rule"],"prefix":"10.1016","volume":"181","author":[{"given":"Nicolas","family":"Peltier","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S0890-5401(03)00016-6_BIB1","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":"1","author":"Bachmair","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB2","series-title":"Proceeding of Computer Science Logic, CSL\u201995","first-page":"130","article-title":"Decision procedures using model building techniques","volume":"vol. 1092","author":"Caferra","year":"1996"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB3","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","article-title":"A method for simultaneous search for refutations and models by equational constraint solving","volume":"13","author":"Caferra","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB4","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1006\/jsco.1999.0360","article-title":"Combining enumeration and deductive techniques in order to increase the class of constructible infinite models","volume":"29","author":"Caferra","year":"1999","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB5","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","article-title":"Equational problems and disunification","volume":"7","author":"Comon","year":"1989","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB6","unstructured":"H. Comon, Unification et Disunification. Th\u00e9orie et Applications, Ph.D. Thesis, INPG, Grenoble, 1988"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB7","series-title":"Computational Logic: Essays in Honor of Alan Robinson","article-title":"Disunification: a survey","author":"Comon","year":"1991"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB8","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, N. Zamov, Resolution Methods for the Decision Problem, LNAI, vol. 679, Springer, Berlin, 1993","DOI":"10.1007\/3-540-56732-1"},{"issue":"1","key":"10.1016\/S0890-5401(03)00016-6_BIB9","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1093\/jigpal\/6.1.17","article-title":"Decision procedures and model building in equational clause logic","volume":"6","author":"Ferm\u00fcller","year":"1998","journal-title":"Journal of the IGPL"},{"issue":"2","key":"10.1016\/S0890-5401(03)00016-6_BIB10","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","article-title":"Hyperresolution and automated model building","volume":"6","author":"Ferm\u00fcller","year":"1996","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB11","series-title":"Handbook of Automated Reasoning","first-page":"1791","article-title":"Resolution decision procedures","author":"Ferm\u00fcller","year":"2001"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB12","series-title":"First-Order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science","author":"Fitting","year":"1990"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB13","unstructured":"L. Georgieva, U. Hustadt, R.A. Schmidt, Hyperresolution for guarded formulae, in: P. Baumgartner, H. Zhang (Eds.) Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000), vol. 5\/2000 of Fachberichte Informatik, Koblenz, Germany, 2000, Institut f\u00fcr Informatik, Universit\u00e4t Koblenz-Landau, pp. 101\u2013112"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB14","series-title":"Automated Deduction\u2014CADE-18","first-page":"258","article-title":"A new clausal class decidable by hyperresolution","volume":"vol. 2392","author":"Georgieva","year":"2002"},{"issue":"2","key":"10.1016\/S0890-5401(03)00016-6_BIB15","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1015067300005","article-title":"Using resolution for testing modal satisfiability and building models","volume":"28","author":"Hustadt","year":"2002","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB16","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","article-title":"Resolution strategies as decision procedures","volume":"23","author":"Joyner","year":"1976","journal-title":"Journal of the ACM"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB17","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/BF00243794","article-title":"Explicit representation of terms defined by counter-examples","volume":"3","author":"Lassez","year":"1987","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB18","series-title":"The Resolution Calculus, Texts in Theoretical Computer Science","author":"Leitsch","year":"1997"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB19","doi-asserted-by":"crossref","first-page":"163","DOI":"10.3233\/FI-1993-182-406","article-title":"Deciding clause classes by semantic clash resolution","volume":"18","author":"Leitsch","year":"1993","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB20","series-title":"Automated Theorem Proving: A Logical Basis","volume":"vol. 6","author":"Loveland","year":"1978"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB21","series-title":"Proceedings of CADE-15","article-title":"An equational constraints solver","author":"Peltier","year":"1998"},{"issue":"2","key":"10.1016\/S0890-5401(03)00016-6_BIB22","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/jigpal\/7.2.217","article-title":"Pruning the search space and extracting more models in tableaux","volume":"7","author":"Peltier","year":"1999","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB23","unstructured":"N. Peltier. Model building with ordered resolution, in: P. Baumgartner, H. Zhang (Eds.), Proceedings of the Third International Workshop First-Order Theorem Proving (FTP\u201900), pp. 158\u2013169. Technical Report, Universit\u00e4t Koblenz-Landau., July 2000, St.-Andrews, Scotland"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB24","unstructured":"N. Peltier, A calculus combining resolution and enumeration for building finite models, Journal of Symbolic Computation (2001), to appear"},{"issue":"4","key":"10.1016\/S0890-5401(03)00016-6_BIB25","doi-asserted-by":"crossref","first-page":"601","DOI":"10.1093\/jigpal\/9.4.569","article-title":"On the decidability of the PVD class with equality","volume":"9","author":"Peltier","year":"2001","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB26","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1006\/jsco.1997.0114","article-title":"Increasing the capabilities of model building by constraint solving with terms with integer exponents","volume":"24","author":"Peltier","year":"1997","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB27","series-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR\u201901)","first-page":"578","article-title":"A general method for using terms schematizations in automated deduction","volume":"vol. 2083","author":"Peltier","year":"2001"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB28","series-title":"Automated Deduction\u2014CADE-16, 16th International Conference on Automated Deduction, Trento, Italy","first-page":"97","article-title":"Solving equational problems efficiently","volume":"vol. 1632","author":"Pichler","year":"1999"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB29","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of Association for Computing Machinery"},{"issue":"4","key":"10.1016\/S0890-5401(03)00016-6_BIB30","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","article-title":"Automatic theorem proving with renamable and semantic resolution","volume":"14","author":"Slagle","year":"1967","journal-title":"Journal of the ACM"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB31","unstructured":"J. Slaney, Finder (finite domain enumerator): notes and guides, Technical Report, Australian National University Automated Reasoning Project, Canberra, 1992"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB32","series-title":"Baltic Computer Science","first-page":"33","article-title":"Using resolution for deciding solvable classes and building finite models","volume":"vol. 502","author":"Tammet","year":"1991"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB33","series-title":"Proceedings of CADE-13","first-page":"275","article-title":"An improving lower bound for the elementary theories of trees","volume":"vol. 1104","author":"Vorobyov","year":"1996"},{"key":"10.1016\/S0890-5401(03)00016-6_BIB34","first-page":"298","article-title":"SEM: a system for enumerating models","volume":"vol. 1","author":"Zhang","year":"1995"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000166?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000166?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,6,5]],"date-time":"2021-06-05T00:13:57Z","timestamp":1622852037000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540103000166"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["S0890540103000166"],"URL":"https:\/\/doi.org\/10.1016\/s0890-5401(03)00016-6","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}