{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:32:51Z","timestamp":1725535971797},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642029585"},{"type":"electronic","value":"9783642029592"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_14","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T05:02:22Z","timestamp":1248498142000},"page":"163-166","source":"Crossref","is-referenced-by-count":16,"title":["Instantiation-Based Automated Reasoning: From Theory to Practice"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"14_CR2","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. In: Third Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability (DISPROVING 2006) (July 2006)"},{"issue":"1","key":"14_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218213006002552","volume":"15","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. International Journal on Artificial Intelligence Tools\u00a015(1), 21\u201352 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-89439-1_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Baumgartner","year":"2008","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: ME(LIA) \u2013 Model evolution with linear integer arithmetic constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol.\u00a05330, pp. 258\u2013273. Springer, Heidelberg (2008)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/11814771_11","volume-title":"Automated Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 125\u2013139. Springer, Heidelberg (2006)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","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, vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/11532231_29","volume-title":"Automated Deduction \u2013 CADE-20","author":"P. Baumgartner","year":"2005","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus with equality. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 392\u2013408. Springer, Heidelberg (2005)"},{"key":"14_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The disconnection method: a confluent integration of unification in the analytic framework. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"key":"14_CR9","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: Proc. of Workshop on Model Computation (MODEL) (2003)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-71070-7_35","volume-title":"Automated Reasoning","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol.\u00a05195, pp. 410\u2013425. Springer, Heidelberg (2008)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/11546207_42","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"T. Eiter","year":"2005","unstructured":"Eiter, T., Faber, W., Traxler, P.: Testing strong equivalence of datalog programs - implementation and examples. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS, vol.\u00a03662, pp. 437\u2013441. Springer, Heidelberg (2005)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proc. of LICS 1999, pp. 295\u2013304 (1999)","DOI":"10.1109\/LICS.1999.782624"},{"key":"14_CR15","first-page":"55","volume-title":"Proc. 18th IEEE Symposium on LICS","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on LICS, pp. 55\u201364. IEEE, Los Alamitos (2003)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-30124-0_9","volume-title":"Computer Science Logic","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 71\u201384. Springer, Heidelberg (2004)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11916277_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Ganzinger","year":"2006","unstructured":"Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol.\u00a04246, pp. 497\u2013511. Springer, Heidelberg (2006)"},{"key":"14_CR18","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"J.N. Hooker","year":"2002","unstructured":"Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first order logic. J. Autom. Reasoning\u00a028, 371\u2013396 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR19","first-page":"152","volume-title":"The Ninth International Conference on Principles of Knowledge Representation and Reasoning","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Motik, B., Sattler, U.: Reducing SHIQ-description logic to disjunctive datalog programs. In: The Ninth International Conference on Principles of Knowledge Representation and Reasoning, pp. 152\u2013162. AAAI Press, Menlo Park (2004)"},{"issue":"2-3","key":"14_CR20","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10817-007-9090-1","volume":"40","author":"Y. Kazakov","year":"2008","unstructured":"Kazakov, Y., Motik, B.: A resolution-based decision procedure for SHOIQ. J. Autom. Reasoning\u00a040(2-3), 89\u2013116 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR21","volume-title":"Volume in memoriam of Harald Ganzinger","author":"K. Korovin","year":"2006","unstructured":"Korovin, K.: An invitation to instantiation-based reasoning: a modular approach. In: Podelski, A., Voronkov, A., Wilhelm, R. (eds.) Volume in memoriam of Harald Ganzinger. Springer, Heidelberg (2006) (invited paper) (to appear)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"14_CR23","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Lee, S.-J., Plaisted, D.: Eliminating duplication with the Hyper-linking strategy. J. Autom. Reasoning\u00a09, 25\u201342 (1992)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR24","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-45653-8_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 142\u2013156. Springer, Heidelberg (2001)"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-45616-3_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS, vol.\u00a02381, pp. 176\u2013190. Springer, Heidelberg (2002)"},{"key":"14_CR26","unstructured":"Pease, A., Sutcliffe, G., Siegel, N., Trac, S.: The annual SUMO reasoning prizes at CASC. In: The First International Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol.\u00a0373 (2008)"},{"key":"14_CR27","unstructured":"P\u00e9rez, J.A.N.: Encoding and Solving Problems in Effectively Propositional Logic. PhD thesis, University of Manchester (2007)"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-73595-3_24","volume-title":"Automated Deduction \u2013 CADE-21","author":"J.A.N. P\u00e9rez","year":"2007","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Encodings of bounded LTL model checking in effectively propositional logic. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 346\u2013361. Springer, Heidelberg (2007)"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-540-71070-7_36","volume-title":"Automated Reasoning","author":"J.A.N. P\u00e9rez","year":"2008","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Proof systems for effectively propositional logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol.\u00a05195, pp. 426\u2013440. Springer, Heidelberg (2008)"},{"key":"14_CR30","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Planning with effectively propositional logic. In: Podelski, A., Voronkov, A., Wilhelm, R. (eds.) Volume in memoriam of Harald Ganzinger. Springer, Heidelberg (to appear) (invited paper)"},{"issue":"3","key":"14_CR31","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D. Plaisted","year":"2000","unstructured":"Plaisted, D., Zhu, Y.: Ordered semantic hyper-linking. J. Autom. Reasoning\u00a025(3), 167\u2013217 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11828563","volume-title":"Volume in memoriam of Harald Ganzinger","author":"R.A. Schmidt","year":"2006","unstructured":"Schmidt, R.A., Hustadt, U.: First-order resolution methods for modal logics. In: Podelski, A., Voronkov, A., Wilhelm, R. (eds.) Volume in memoriam of Harald Ganzinger. LNCS. Springer, Heidelberg (2006) (invited overview paper) (to appear)"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-45616-3_24","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"G. Stenz","year":"2002","unstructured":"Stenz, G.: DCTP 1.2 - system abstract. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS, vol.\u00a02381, pp. 335\u2013340. Springer, Heidelberg (2002)"},{"issue":"1","key":"14_CR34","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/AIC-2009-0441","volume":"22","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The 4th IJCAR automated theorem proving system competition - CASC-J4. AI Communications\u00a022(1), 59\u201372 (2009)","journal-title":"AI Communications"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,21]],"date-time":"2020-05-21T00:03:17Z","timestamp":1590019397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}