{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T04:14:36Z","timestamp":1744085676926,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642316050"},{"type":"electronic","value":"9783642316067"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31606-7_26","type":"book-chapter","created":{"date-parts":[[2012,8,25]],"date-time":"2012-08-25T07:47:55Z","timestamp":1345880875000},"page":"301-312","source":"Crossref","is-referenced-by-count":0,"title":["Crossing the Syntactic Barrier: Hom-Disequalities for ${\\mathcal H}_1$-Clauses"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Reu\u00df","sequence":"first","affiliation":[]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"1","key":"26_CR2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3233\/JCS-2005-13104","volume":"13","author":"M. Bugliesi","year":"2005","unstructured":"Bugliesi, M., Rossi, S.: Non-interference proof techniques for the analysis of cryptographic protocols. Journal of Computer Security\u00a013(1), 87\u2013113 (2005)","journal-title":"Journal of Computer Security"},{"key":"26_CR3","unstructured":"Chatzikokolakis, K.: Probabilistic and Information-Theoretic Approaches to Anonymity. Ph.D. thesis, \u00c9cole polytechnique (2007)"},{"key":"26_CR4","unstructured":"Fr\u00fchwirth, T.W., Shapiro, E.Y., Vardi, M.Y., Yardeni, E.: Logic programs as types for logic programs. In: LICS, pp. 314\u2013328 (1991)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Godoy, G., Gim\u00e9nez, O., Ramos, L., \u00c0lvarez, C.: The hom problem is decidable. In: STOC, pp. 485\u2013494. ACM (2010)","DOI":"10.1145\/1806689.1806757"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"issue":"3","key":"26_CR7","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1016\/j.ipl.2005.04.007","volume":"95","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J.: Deciding H1 by resolution. IPL\u00a095(3), 401\u2013408 (2005)","journal-title":"IPL"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30579-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Parrennes, F.: Cryptographic Protocol Analysis on Real C Code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 363\u2013379. Springer, Heidelberg (2005)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-45789-5_5","volume-title":"Static Analysis","author":"F. Nielson","year":"2002","unstructured":"Nielson, F., Riis Nielson, H., Seidl, H.: Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 20\u201335. Springer, Heidelberg (2002)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/978-3-642-16242-8_41","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Reu\u00df","year":"2010","unstructured":"Reu\u00df, A., Seidl, H.: Bottom-Up Tree Automata with Term Constraints. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 581\u2013593. Springer, Heidelberg (2010)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/3-540-48168-0_34","volume-title":"Computer Science Logic","author":"H. Seidl","year":"1999","unstructured":"Seidl, H., Neumann, A.: On Guarding Nested Fixpoints. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 484\u2013498. Springer, Heidelberg (1999)"},{"issue":"20","key":"26_CR12","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1016\/j.ipl.2011.07.011","volume":"111","author":"H. Seidl","year":"2011","unstructured":"Seidl, H., Reu\u00df, A.: Extending H1-clauses with disequalities. IPL\u00a0111(20), 1007\u20131013 (2011)","journal-title":"IPL"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-28729-9_11","volume-title":"Foundations of Software Science and Computational Structures","author":"H. Seidl","year":"2012","unstructured":"Seidl, H., Reu\u00df, A.: Extending ${\\cal H}_1$-Clauses with Path Disequalities. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol.\u00a07213, pp. 165\u2013179. Springer, Heidelberg (2012)"},{"key":"26_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31606-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T07:47:47Z","timestamp":1744012067000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-31606-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316050","9783642316067"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31606-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}