{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:03Z","timestamp":1747592463345},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_13","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:34:07Z","timestamp":1499679247000},"page":"202-219","source":"Crossref","is-referenced-by-count":4,"title":["Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Teucke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217\u2013247 (1994). Revised version of Max-Planck-Institut f\u00fcr Informatik Technical report, MPI-I-91-208 (1991)","journal-title":"J. Logic Comput."},{"issue":"6","key":"13_CR2","doi-asserted-by":"crossref","first-page":"1007","DOI":"10.1145\/293347.293352","volume":"45","author":"L Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. ACM 45(6), 1007\u20131049 (1998)","journal-title":"J. ACM"},{"issue":"2&3","key":"13_CR3","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0304-3975(89)90006-6","volume":"67","author":"JCM Baeten","year":"1989","unstructured":"Baeten, J.C.M., Bergstra, J.A., Klop, J., Weijland, W.P.: Term-rewriting systems with rule priorities. Theor. Comput. Sci. 67(2&3), 283\u2013301 (1989)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"13_CR4","doi-asserted-by":"crossref","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. Int. J. Artif. Intell. Tools 15(1), 21\u201352 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 2741, pp. 350\u2013364. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-45085-6_32"},{"key":"13_CR6","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007). \nhttp:\/\/www.grappa.univ-lille3.fr\/tata\n\n. Accessed 12 Oct 2007"},{"issue":"3","key":"13_CR7","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1016\/j.ipl.2005.04.007","volume":"95","author":"J Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J.: Deciding \n            $$\\cal{H}_1$$\n           by resolution. Inf. Process. Lett. 95(3), 401\u2013408 (2005)","journal-title":"Inf. Process. Lett."},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0052362","volume-title":"Rewriting Techniques and Applications","author":"F Jacquemard","year":"1998","unstructured":"Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in extensions of shallow equational theories. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 76\u201390. Springer, Heidelberg (1998). doi:\n10.1007\/BFb0052362"},{"key":"13_CR9","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 \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-71070-7_24"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Inst-Gen \u2013 a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239\u2013270. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-37651-1_10"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-39799-8_1"},{"issue":"20","key":"13_CR12","doi-asserted-by":"crossref","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. Inf. Process. Lett. 111(20), 1007\u20131013 (2011)","journal-title":"Inf. Process. Lett."},{"key":"13_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, FoSSaCS 2012","author":"H Seidl","year":"2012","unstructured":"Seidl, H., Reu\u00df, A.: Extending \n            $${\\cal{H}_1}$$\n          -clauses with path disequalities. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 165\u2013179. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-28729-9_11"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-71322-7_5","volume-title":"Program Analysis and Compilation, Theory and Practice","author":"H Seidl","year":"2007","unstructured":"Seidl, H., Verma, K.N.: Cryptographic protocol verification using tractable classes of horn clauses. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol. 4444, pp. 97\u2013119. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-71322-7_5"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Slaney, J.K., Surendonk, T.: Combining finite model generation with theorem proving: problems and prospects. In: Baader, F., Schulz, K.U. (eds.), Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26-29, 1996, Proceedings, vol. 3. Applied Logic Series, pp. 141\u2013155. Kluwer Academic Publishers (1996)","DOI":"10.1007\/978-94-009-0349-4_7"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-14203-1_38","volume-title":"Automated Reasoning","author":"M Suda","year":"2010","unstructured":"Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 441\u2013456. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-14203-1_38"},{"issue":"4","key":"13_CR17","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF Parts, v3.5.0. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-24246-0_6","volume-title":"Frontiers of Combining Systems","author":"A Teucke","year":"2015","unstructured":"Teucke, A., Weidenbach, C.: First-order logic theorem proving and model building via approximation and instantiation. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 85\u2013100. Springer, Cham (2015). doi:\n10.1007\/978-3-319-24246-0_6"},{"key":"13_CR19","unstructured":"Teucke, A., Weidenbach, C.: Ordered resolution with straight dismatching constraints. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning Co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, 2 July 2016, vol. 1635. CEUR Workshop Proceedings, pp. 95\u2013109 (2016). \nCEUR-WS.org"},{"key":"13_CR20","unstructured":"Teucke, A., Weidenbach, C.: Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints (2017). \nhttp:\/\/arxiv.org\/abs\/1703.02837"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_46"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction \u2014 CADE-16","author":"C Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. CADE 1999. LNCS, vol. 1632, pp. 314\u2013328. Springer, Heidelberg (1999). doi:\n10.1007\/3-540-48660-7_29"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:37:24Z","timestamp":1499679444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}