{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T06:58:14Z","timestamp":1758265094925,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_28","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"303-317","source":"Crossref","is-referenced-by-count":22,"title":["Geometric Resolution: A Proof Procedure Based on Finite Model Search"],"prefix":"10.1007","author":[{"given":"Hans","family":"de Nivelle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jia","family":"Meng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"28_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. Journal of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"28_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"28_CR3","unstructured":"Bezem, M.: Disproving distributivity in lattices using geometric logic. In: Workshop on Disproving, Non-Theorems, Non-Validity, Non-Provability, informal proceedings, July 2005, pp. 24\u201331 (2005)"},{"key":"28_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/11591191_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Bezem","year":"2005","unstructured":"Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 246\u2013260. Springer, Heidelberg (2005)"},{"key":"28_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/3-540-49545-2_9","volume-title":"Logics in Artificial Intelligence","author":"F. Bry","year":"1998","unstructured":"Bry, F., Torge, S.: A deduction method complete for refutation and finite satisfiability. In: Dix, J., Fari\u00f1as del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol.\u00a01489, pp. 122\u2013138. Springer, Heidelberg (1998)"},{"issue":"1","key":"28_CR6","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(02)00092-5","volume":"35","author":"H. Nivelle de","year":"2003","unstructured":"de Nivelle, H., de Rijke, M.: Deciding the guarded fragments by resolution. Journal of Symbolic Computation\u00a035(1), 21\u201358 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: LICS 1999, pp. 295\u2013303 (1999)","DOI":"10.1109\/LICS.1999.782624"},{"key":"28_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-25984-8_7","volume-title":"Automated Reasoning","author":"Y. Kazakov","year":"2004","unstructured":"Kazakov, Y., de Nivelle, H.: A resolution decision procedure for the guarded fragment with transitive guards. In: IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 122\u2013136. Springer, Heidelberg (2004)"},{"key":"28_CR9","first-page":"162","volume-title":"Proceedings of AAAI 1994","author":"S. Kim","year":"1994","unstructured":"Kim, S., Zhang, H.: ModGen: Theorem proving by model generation. In: Hayes-Roth, B., Korf, R. (eds.) Proceedings of AAAI 1994, pp. 162\u2013167. AAAI Press, Menlo Park (1994)"},{"key":"28_CR10","unstructured":"McCune, W.: Models and counter examples MACE2 (system), http:\/\/www-unix.mcs.anl.gov\/AR\/mace2\/"},{"key":"28_CR11","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine oriented logic based on the resolution principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"28_CR12","unstructured":"Slaney, J.: Scott: A model-guided theorem prover. In: IJCAI 1993, pp. 109\u2013114 (1993)"},{"key":"28_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00244457","volume":"17","author":"J. Zhang","year":"1996","unstructured":"Zhang, J.: Constructing finite algebras with FALCON. Journal of Automated Reasoning\u00a017, 1\u201322 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR14","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: IJCAI, pp. 298\u2013303 (1995)"},{"key":"28_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/3-540-45620-1_26","volume-title":"Automated Deduction - CADE-18","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 295\u2013313. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:08:46Z","timestamp":1736575726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11814771_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}