{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:06Z","timestamp":1725490866906},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_21","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"311-327","source":"Crossref","is-referenced-by-count":5,"title":["Labelled Clauses"],"prefix":"10.1007","author":[{"given":"Tal","family":"Lev-Ami","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"key":"21_CR2","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-4040-9","volume-title":"Labelled Deduction","author":"D. Basin","year":"2000","unstructured":"Basin, D., D\u2019Agostino, M., Gabbay, D.M., Matthews, S., Vigan\u00f2, L.: Labelled Deduction. Applied Logic Series, vol.\u00a017. Kluwer, Dordrecht (2000)"},{"issue":"2","key":"21_CR3","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.jsc.2004.11.001","volume":"39","author":"M.P. Bonacina","year":"2005","unstructured":"Bonacina, M.P.: Towards a unified model of search in theorem-proving: subgoal-reduction strategies. J. Symb. Comput.\u00a039(2), 209\u2013255 (2005)","journal-title":"J. Symb. Comput."},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"21_CR6","first-page":"183","volume":"4","author":"C. Green","year":"1969","unstructured":"Green, C.: Theorem-proving by resolution as a basis for question-answering systems. Machine Intelligence\u00a04, 183\u2013205 (1969)","journal-title":"Machine Intelligence"},{"key":"21_CR7","first-page":"103","volume-title":"Handbook of Automated Reasoning, ch. 6","author":"R. H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 6, vol.\u00a01, pp. 103\u2013177. Elsevier, North-Holland (2001)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/11513988_5","volume-title":"Computer Aided Verification","author":"S. Lahiri","year":"2005","unstructured":"Lahiri, S., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 24\u201338. Springer, Heidelberg (2005)"},{"key":"21_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, Springer, Heidelberg (2000)"},{"key":"21_CR11","unstructured":"Lev-Ami, T., Weidenbach, C., Reps, T., Sagiv, M.: Experimental version of SPASS for multiple conjectures (2007), Available at http:\/\/www.cs.tau.ac.il\/~tla\/SPASS"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Nelson, C.G., Oppen, D.C.: A simplifier based on efficient decision algorithms. In: POPL, pp. 141\u2013150 (1978)","DOI":"10.1145\/512760.512775"},{"key":"21_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/11591191_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 23\u201346. Springer, Heidelberg (2005)"},{"key":"21_CR15","unstructured":"Riazanov, A., Voronkov, A.: Splitting without backtracking. In: IJCAI, pp. 611\u2013617 (2001)"},{"issue":"2-3","key":"21_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-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS, 217\u2013298 (2002)","DOI":"10.1145\/514188.514190"},{"issue":"2\/3","key":"21_CR18","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"21_CR19","unstructured":"Voronkov, A.: Personal communication (2007)"},{"key":"21_CR20","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, ch. 27","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 27, vol.\u00a02, pp. 1965\u20132012. Elsevier, North-Holland (2001)"},{"key":"21_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS version 2.0. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, pp. 275\u2013279. Springer, Heidelberg (2002)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: A new incremental satisfiability engine. In: DAC, pp. 542\u2013545 (2001)","DOI":"10.1145\/378239.379019"},{"key":"21_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/BFb0057466","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications","author":"A. Wolf","year":"1998","unstructured":"Wolf, A.: Strategy selection for automated theorem proving. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol.\u00a01480, pp. 452\u2013465. Springer, Heidelberg (1998)"},{"issue":"4","key":"21_CR24","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM\u00a012(4), 536\u2013541 (1965)","journal-title":"J. ACM"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:04Z","timestamp":1619502784000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}