{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:47:56Z","timestamp":1762458476955},"reference-count":5,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Artif. Intell. Tools"],"published-print":{"date-parts":[[2006,2]]},"abstract":"<jats:p> Darwin is the first implementation of the Model Evolution Calculus by Baumgartner and Tinelli. The Model Evolution Calculus lifts the DPLL procedure to first-order logic. Darwin is meant to be a fast and clean implementation of the calculus, showing its effectiveness and providing a base for further improvements and extensions. <\/jats:p><jats:p> Based on a brief summary of the Model Evolution Calculus, we describe in the main part of the paper Darwin's proof procedure and its data structures and algorithms, discussing the main design decisions and features that influence Darwin's performance. We also report on practical experiments carried out with problems from the CASC-J2 system competition and parts of the TPTP Problem Library, and compare the results with those of other state-of-the-art theorem provers. <\/jats:p>","DOI":"10.1142\/s0218213006002552","type":"journal-article","created":{"date-parts":[[2006,1,24]],"date-time":"2006-01-24T11:15:46Z","timestamp":1138101346000},"page":"21-52","source":"Crossref","is-referenced-by-count":36,"title":["IMPLEMENTING THE MODEL EVOLUTION CALCULUS"],"prefix":"10.1142","volume":"15","author":[{"given":"PETER","family":"BAUMGARTNER","sequence":"first","affiliation":[{"name":"Programming Logics Group, Max-Planck-Institut f\u00fcr Informatik, Stuhlsatzenhausweg 85, 66123 Saarbr\u00fccken, Germany"}]},{"given":"ALEXANDER","family":"FUCHS","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Iowa, 14 MacLean Hall, Iowa City, Iowa 52242, USA"}]},{"given":"CESARE","family":"TINELLI","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Iowa, 14 MacLean Hall, Iowa City, Iowa 52242, USA"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"rf7","first-page":"69","volume":"4","author":"Oppacher F.","journal-title":"Journal of Automated Reasoning"},{"key":"rf19","unstructured":"R.\u00a0Sekar, I. V.\u00a0Ramakrishnan and A.\u00a0Voronkov, Handbook of Automated Reasoning\u00a0II (Elsevier Science, 2001)\u00a0pp. 1855\u20131964."},{"key":"rf22","unstructured":"R.\u00a0Letz and G.\u00a0Stenz, Handbook of Automated Reasoning, eds. A.\u00a0Robinson and A.\u00a0Voronkov (Elsevier, 2001)\u00a0pp. 2017\u20132114."}],"container-title":["International Journal on Artificial Intelligence Tools"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218213006002552","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T02:30:59Z","timestamp":1565145059000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218213006002552"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2]]},"references-count":5,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2006,2]]}},"alternative-id":["10.1142\/S0218213006002552"],"URL":"https:\/\/doi.org\/10.1142\/s0218213006002552","relation":{},"ISSN":["0218-2130","1793-6349"],"issn-type":[{"value":"0218-2130","type":"print"},{"value":"1793-6349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2]]}}}