{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:40:36Z","timestamp":1725518436971},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_36","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"426-440","source":"Crossref","is-referenced-by-count":9,"title":["Proof Systems for Effectively Propositional Logic"],"prefix":"10.1007","author":[{"given":"Juan Antonio","family":"Navarro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"36_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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":"36_CR2","series-title":"Lecture Notes in Artificial Intelligence","first-page":"110","volume-title":"TABLEAUX 2006: Proceedings of the International Conference on Automated Reasoning 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: TABLEAUX 2006: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Terrasini, Italy. LNCS (LNAI), vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"key":"36_CR3","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: MODEL 2003: Proceedings of the Workshop on Model Computation (2003)"},{"key":"36_CR4","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"36_CR5","unstructured":"Fuchs, A.: Darwin: A theorem prover for the model evolution calculus. Master\u2019s thesis, University of Koblenz-Landau (2004)"},{"key":"36_CR6","first-page":"55","volume-title":"LICS 2003: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science","author":"H. Ganzinger","year":"1884","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: LICS 2003: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, Ottawa, Canada, June 2003, vol.\u00a02, p. 55. IEEE Computer Society, Los Alamitos (1884)"},{"issue":"3","key":"36_CR7","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. Journal of Automated Reasoning\u00a028(3), 371\u2013396 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"36_CR8","unstructured":"Korovin, K.: Implementing an instantiation-based theorem prover for first-order logic. In: Benzmueller, C., Fischer, B., Sutcliffe, G. (eds.) IWIL 2006: Proceedings of the 6th International Workshop on the Implementation of Logics, held at the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2006). CEUR Workshop Proceedings, Phnom Penh, Cambodia, vol.\u00a0212 (2006), \n                    \n                      http:\/\/www.cs.man.ac.uk\/~korovink\/iprover\/"},{"issue":"1","key":"36_CR9","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.A.: Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning\u00a09(1), 25\u201342 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"36_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/3-540-45744-5_30","volume-title":"Automated Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: DCTP: A disconnection calculus theorem prover. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 381\u2013385. Springer, Heidelberg (2001)"},{"key":"36_CR11","series-title":"Lecture Notes in Artificial Intelligence","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. Navarro P\u00e9rez","year":"2007","unstructured":"Navarro P\u00e9rez, J.A., Voronkov, A.: Encodings of bounded LTL model checking in effectively propositional logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 346\u2013361. Springer, Heidelberg (2007)"},{"key":"36_CR12","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Planning with effectively propositional logic. In: Collection of Papers Dedicated to Harald Ganzinger\u2019s Memory (to appear, 2007)"},{"issue":"2","key":"36_CR13","first-page":"79","volume":"15","author":"F.J. Pelletier","year":"2002","unstructured":"Pelletier, F.J., Sutcliffe, G., Suttner, C.B.: The development of CASC. AI Communications\u00a015(2), 79\u201390 (2002)","journal-title":"AI Communications"},{"issue":"3","key":"36_CR14","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D.A. Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyper-linking. Journal of Automated Reasoning\u00a025(3), 167\u2013217 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"Plaisted, D.A., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Computational Intelligence. Vieweg, Wiesbaden, Germany (1997)","DOI":"10.1007\/978-3-322-93862-6"},{"issue":"2","key":"36_CR16","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications\u00a015(2), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"36_CR17","first-page":"72","volume-title":"FLAIRS 2002: Proceedings of the Fifteenth International Florida Artificial Intelligence Research Society Conference","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: A comparison of different techniques for grounding near-propositional CNF formulae. In: Haller, S., Simmons, G. (eds.) FLAIRS 2002: Proceedings of the Fifteenth International Florida Artificial Intelligence Research Society Conference, pp. 72\u201376. AAAI Press, Menlo Park (2002)"},{"key":"36_CR18","unstructured":"Sutcliffe, G.: The CADE-21 ATP system competition website (2007), \n                    \n                      http:\/\/www.cs.miami.edu\/~tptp\/CASC\/21\/"},{"issue":"2","key":"36_CR19","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"36_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-540-39715-1_10","volume-title":"Rules and Rule Markup Languages for the Semantic Web","author":"T. Tammet","year":"2003","unstructured":"Tammet, T., Kadarpik, V.: Combining an inference engine with database: A rule server. In: Schr\u00f6der, M., Wagner, G. (eds.) RuleML 2003. LNCS, vol.\u00a02876, pp. 136\u2013149. Springer, Heidelberg (2003)"},{"key":"36_CR21","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Merging relational database technology with the constraint technology. In: Perspectives of System Informatics. Andrei Ershov Second International Memorial Conference (Preliminary Proceedings), Novosibirsk, Akademgorodok, Russia, June 1996, pp. 189\u2013195 (1996)","DOI":"10.1007\/3-540-62064-8_34"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:36:33Z","timestamp":1620016593000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}