{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:29:07Z","timestamp":1725488947060},"publisher-location":"Berlin, Heidelberg","reference-count":15,"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_18","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"211-225","source":"Crossref","is-referenced-by-count":7,"title":["Deductive Search for Errors in Free Data Type Specifications Using Model Generation"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"18_CR1","unstructured":"Wolfgang Ahrendt. Deduktive Fehlersuche in Abstrakten Datentypen. 2001. Dissertation (preversion, in German), University of Karlsruhe, available under \n                    http:\/\/www.cs.chalmers.se\/~ahrendt\/cade02\/diss.ps.gz\n                    \n                  ."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair. Proof by consistency in equational theories. In Proc. Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, pages 228\u2013233. IEEE Press, 1988.","DOI":"10.1109\/LICS.1988.5122"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Bry and Sunna Torge. A deduction method complete for refutation and finite satisfiability. In Proc. 6th European Workshop on Logics in AI (JELIA), volume 1489 of LNAI, pages 122\u2013136. Springer-Verlag, 1998.","DOI":"10.1007\/3-540-49545-2_9"},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1006\/jsco.1999.0360","volume":"29","author":"R. Caferra","year":"2000","unstructured":"Ricardo Caferra and Nicolas Peltier. Combining enumeration and deductive techniques in order to increase the class of constructible infinite models. Journal of Symbolic Computation, 29:177\u2013211, 2000.","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR5","unstructured":"Hiroshi Fujita and Ryuzo Hasegawa. A model generation theorem prover in KL1 using a ramified-stack algorithm. In Koichi Furukawa, editor, Proceedings 8th International Conference on Logic Programming, Paris\/France, pages 535\u2013548. MIT Press, 1991."},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Christian Ferm\u00fcller and Alexander Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2), 1996.","DOI":"10.1093\/logcom\/6.2.173"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Martin Giese and Wolfgang Ahrendt. Hilbert\u2019s \u2208-terms in Automated Theorem Proving. In Neil V. Murray, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, Saratoga Springs, USA, volume 1617 of LNAI, pages 171\u2013185. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48754-9_17"},{"key":"18_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"Proceedings 9th Conference on Automated Deduction","author":"R. Manthey","year":"1988","unstructured":"Rainer Manthey and Fran\u00e7ois Bry. SATCHMO: A theorem prover implemented in Prolog. In Proceedings 9th Conference on Automated Deduction, volume 310 of LNCS, pages 415\u2013434. Springer-Verlag, 1988."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Raul Monroy, Alan Bundy, and Andrew Ireland. Proof plans for the correction of false conjectures. In Frank Pfenning, editor, Proc. 5th International Conference on Logic Programming and Automated Reasoning, Kiev, Ukraine, volume 822 of LNAI, pages 54\u201368. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58216-9_29"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Martin Protzen. Disproving conjectures. In D. Kapur, editor, Proc. 11th CADE, Albany\/NY, USA, volume 607 of LNAI, pages 340\u2013354. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_176"},{"key":"18_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/3-540-61511-3_70","volume-title":"Proc. 13th CADE, New Brunswick\/NJ, USA","author":"M. Protzen","year":"1996","unstructured":"Martin Protzen. Patching faulty conjectures. In Michael McRobbie and John Slaney, editors, Proc. 13th CADE, New Brunswick\/NJ, USA, volume 1104 of LNCS, pages 77\u201391. Springer-Verlag, 1996."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Wolfgang Reif, Gerhard Schellhorn, and Andreas Thums. Flaw detection in formal specifications. In Rajeev Gor\u00e9, Alexander Leitsch, and Tobias Nipkow, editors, Automated Reasoning, IJCAR 2001 Siena, Italy, June 18\u201323, 2001 Proceedings, volume 2083 of LNAI. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_52"},{"key":"18_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1007\/3-540-58156-1_63","volume-title":"Proc. 12th CADE, Nancy\/France","author":"J. Slaney","year":"1994","unstructured":"John Slaney. FINDER: finite domain enumerator. In Alan Bundy, editor, Proc. 12th CADE, Nancy\/France, volume 814 of LNCS, pages 798\u2013801. Springer-Verlag, 1994."},{"key":"18_CR14","unstructured":"Andreas Thums. Fehlersuche in Formalen Spezifikationen. diploma thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Ulm, 1998."},{"key":"18_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/3-540-61314-5","volume-title":"Proc. 13th CADE, New Brunswick\/NJ, USA","author":"J. Zhang","year":"1996","unstructured":"Jian Zhang and Hantao Zhang. Generating models by SEM. In Michael McRobbie and John Slaney, editors, Proc. 13th CADE, New Brunswick\/NJ, USA, volume 1104 of LNCS, pages 309\u2013327. Springer-Verlag, 1996."}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T11:51:11Z","timestamp":1550749871000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}