{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T04:55:51Z","timestamp":1725684951934},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642298219"},{"type":"electronic","value":"9783642298226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29822-6_16","type":"book-chapter","created":{"date-parts":[[2012,5,20]],"date-time":"2012-05-20T13:21:09Z","timestamp":1337520069000},"page":"182-196","source":"Crossref","is-referenced-by-count":1,"title":["Mutual Exclusion by Interpolation"],"prefix":"10.1007","author":[{"given":"Jael","family":"Kriener","sequence":"first","affiliation":[]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-31987-0_9","volume-title":"Programming Languages and Systems","author":"L. Lu","year":"2005","unstructured":"Lu, L., King, A.: Determinacy Inference for Logic Programs. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 108\u2013123. Springer, Heidelberg (2005)"},{"key":"16_CR2","first-page":"537","volume":"11","author":"J. Kriener","year":"2011","unstructured":"Kriener, J., King, A.: RedAlert: Determinacy Inference for Prolog. TPLP\u00a011, 537\u2013553 (2011)","journal-title":"TPLP"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(92)00019-N","volume":"124","author":"A. Bossi","year":"1994","unstructured":"Bossi, A., Cocco, N., Fabris, M.: Norms on Terms and their use in Proving Universal Termination of a Logic Program. TCS\u00a0124, 297\u2013328 (1994)","journal-title":"TCS"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/3-540-62718-9_13","volume-title":"Logic Program Synthesis and Transformation","author":"J.C. Martin","year":"1997","unstructured":"Martin, J.C., King, A., Soper, P.: Typed Norms for Typed Logic Programs. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, pp. 224\u2013238. Springer, Heidelberg (1997)"},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The Complexity of Linear Problems in Fields. Journal of Symbolic Computation\u00a05, 3\u201327 (1988)","journal-title":"Journal of Symbolic Computation"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. J. Symb. Log.\u00a022, 269\u2013285 (1957)","journal-title":"J. Symb. Log."},{"key":"16_CR7","unstructured":"Weissenbacher, G.: Program Analysis with Interpolants. PhD thesis, Magdalen College (2010), \n                  \n                    http:\/\/ora.ouls.ox.ac.uk\/objects\/uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. J. Symb. Log.\u00a062, 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"key":"16_CR9","first-page":"1","volume":"124","author":"J. Farkas","year":"1902","unstructured":"Farkas, J.: Theorie der einfachen Ungleichungen. Journal f\u00fcr die Reine und Angewandte Mathematik\u00a0124, 1\u201327 (1902)","journal-title":"Journal f\u00fcr die Reine und Angewandte Mathematik"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Avis, D.: lrs: A Revised Implementation of the Reverse Search Vertex Enumeration Algorithm. In: Kalai, G., Ziegler, G.M. (eds.) Polytopes - Combinatorics and Computation, pp. 177\u2013198. Birkhauser-Verlag (2000)","DOI":"10.1007\/978-3-0348-8438-9_9"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Goodman, J.E., O\u2019Rourke, J. (eds.): Handbook of Discrete and Computational Geometry. CRC Press (2004)","DOI":"10.1201\/9781420035315"},{"key":"16_CR12","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0167-5060(08)70325-X","volume":"2","author":"R.C. Read","year":"1978","unstructured":"Read, R.C.: Everyone a Winner. Annals of Discrete Mathematics\u00a02, 107\u2013120 (1978)","journal-title":"Annals of Discrete Mathematics"},{"key":"16_CR13","unstructured":"Peyton-Jones, S., Jones, M., Meijer, E.: Type Classes: an exploration of the design space. In: ACM SIGPLAN Haskell Workshop (1997)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Morris, J.G., Jones, M.P.: Instance Chains: Type Class Programming Without Overlapping Instances. In: Hudak, P., Weirich, S. (eds.) ICFP, pp. 375\u2013386. ACM (2010)","DOI":"10.1145\/1932681.1863596"},{"key":"16_CR15","unstructured":"The\u00a0GHC\u00a0Team: The Glorious Glasgow Haskell Compilation System User\u2019s Guide, Version 7.2.1 (2011), \n                  \n                    http:\/\/www.haskell.org\/ghc\/docs\/latest\/html\/users_guide"},{"key":"16_CR16","unstructured":"O\u2019Keefe, R.A.: The Craft of Prolog. MIT Press (1990)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-540-24599-5_22","volume-title":"Logic Programming","author":"A. King","year":"2003","unstructured":"King, A., Lu, L.: Forward versus Backward Verification of Logic Programs. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol.\u00a02916, pp. 315\u2013330. Springer, Heidelberg (2003)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 199\u2013213. Springer, Heidelberg (2009)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Ziegler, G.M.: Lectures on Polytopes. Springer, New York (1995)","DOI":"10.1007\/978-1-4613-8431-1"},{"key":"16_CR20","unstructured":"Bertsimas, D., Tsitsiklis, J.: Introduction to Linear Optimization, 1st edn. Athena Scientific (1997)"},{"key":"16_CR21","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0166-218X(95)00026-N","volume":"65","author":"D. Avis","year":"1996","unstructured":"Avis, D., Fukuda, K.: Reverse search for enumeration. Discrete Applied Mathematics\u00a065, 21\u201346 (1996)","journal-title":"Discrete Applied Mathematics"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-62718-9_12","volume-title":"Logic Program Synthesis and Transformation","author":"F. Benoy","year":"1997","unstructured":"Benoy, F., King, A.: Inferring Argument Size Relationships with CLP(R). In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, pp. 204\u2013223. Springer, Heidelberg (1997)"},{"key":"16_CR23","first-page":"31","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The Octagon Abstract Domain. HOSC\u00a019, 31\u2013100 (2006)","journal-title":"HOSC"},{"key":"16_CR24","first-page":"41","volume":"2","author":"M. Sozeau","year":"2009","unstructured":"Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning\u00a02, 41\u201362 (2009)","journal-title":"Journal of Formalized Reasoning"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Sahlin, D.: Determinacy Analysis for Full Prolog. In: Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 23\u201330. ACM (1991)","DOI":"10.1145\/115866.115869"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/3-540-62064-8_31","volume-title":"Perspectives of System Informatics","author":"T.\u00c6. Mogensen","year":"1996","unstructured":"Mogensen, T.\u00c6.: A Semantics-Based Determinacy Analysis for Prolog with Cut. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) PSI 1996. LNCS, vol.\u00a01181, pp. 374\u2013385. Springer, Heidelberg (1996)"},{"key":"16_CR27","unstructured":"Dawson, S., Ramakrishnan, C.R., Ramakrishnan, I.V., Sekar, R.C.: Extracting Determinacy in Logic Programs. In: Proceedings of the Tenth International Conference on Logic Programming, pp. 424\u2013438. MIT Press (1993)"},{"key":"16_CR28","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s00354-008-0085-1","volume":"28","author":"P. L\u00f3pez-Garc\u00eda","year":"2010","unstructured":"L\u00f3pez-Garc\u00eda, P., Bueno, F., Hermenegildo, M.V.: Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Analyses. New Generation Computing\u00a028, 177\u2013206 (2010)","journal-title":"New Generation Computing"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig Interpolants in Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"16_CR30","doi-asserted-by":"publisher","first-page":"1212","DOI":"10.1016\/j.jsc.2010.06.005","volume":"45","author":"A. Rybalchenko","year":"2010","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. Journal of Symbolic Computation\u00a045, 1212\u20131233 (2010)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29822-6_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:17:27Z","timestamp":1620127047000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29822-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642298219","9783642298226"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29822-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}