{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:29:04Z","timestamp":1725488944286},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_19","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"226-240","source":"Crossref","is-referenced-by-count":5,"title":["Reasoning by Symmetry and Function Ordering in Finite Model Generation"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Audemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Belaid","family":"Benhamou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"G. Audemard and L. Henocque. The extended least number heuristic. Proceedings of the first International Joint Conference in Automated Reasoning (IJCAR), Springer Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_35"},{"issue":"1\u20132","key":"19_CR2","doi-asserted-by":"crossref","first-page":"21","DOI":"10.3233\/FI-1999-391202","volume":"39","author":"B. Benhamou","year":"1999","unstructured":"B. Benhamou and L. Henocque. A hybrid method for finite model search in equational theories. Fundamenta Informaticae, 39(1\u20132):21\u201338, 1999.","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"19_CR3","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/BF00881844","volume":"12","author":"B. Benhamou","year":"1994","unstructured":"B. Benhamou and L. Sais. Tractability through symmetries in propositional calculus. Journal of Automated Reasoning, 12(1):89\u2013102, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR4","unstructured":"J. Crawford. A theorical analisys of reasoning by symmetry in first-order logic. In Proceedings of Workshop on Tractable Reasonning, AAI92, pages 17\u201322, 1992."},{"key":"19_CR5","unstructured":"J. Crawford, M. L. Ginsberg, E. Luck, and A. Roy. Symmetry-breaking predicates for search problems. In proceedings of KR\u201996, pages 148\u2013159. 1996."},{"key":"19_CR6","unstructured":"M. Fujita, J. Slaney, and F. Bennett. Automatic generation of some results in finite algebra. In Proceedings of International Joint Conference on Artificial Intelligence, pages 52\u201357. Morgan Kaufmann, 1993."},{"issue":"4","key":"19_CR7","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/8.4.511","volume":"8","author":"N. Peltier","year":"1998","unstructured":"N. Peltier. A new method for automated finite model building exploiting failures and symmetries. Journal of Logic and Computation, 8(4):511\u2013543, 1998.","journal-title":"Journal of Logic and Computation"},{"key":"19_CR8","unstructured":"C. Suttner and G. Sutcliffe. The TPTP Problem Library. Technical Report, J. Cook University, 1997. http:\/\/www.cs.jcu.edu.au\/ftp\/pub\/techreports\/97-8.ps.gz"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"J. Zhang. Problems on the Generation of Finite Models. In proceedings of the 12th International Conference on Automated Deduction, LNAI 814, pages 753\u2013757, Nancy, France, 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58156-1_54"},{"issue":"1","key":"19_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00244457","volume":"17","author":"J. Zhang","year":"1996","unstructured":"J. Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17(1):1\u201322, August 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR11","unstructured":"J. Zhang. Test Problems and Perl Script for Finite Model Searching. Association of Automated Reasoning, Newsletter 47, 2000. http:\/\/www-unix.mcs.anl.gov\/AAR\/issueapril00\/issueapril00.html"},{"key":"19_CR12","unstructured":"J. Zhang and Hantao Zhang. SEM: a system for enumerating models. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pages 298\u2013303, 1995."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T20:26:44Z","timestamp":1587846404000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}