{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:47Z","timestamp":1740123287292,"version":"3.37.3"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,2,25]],"date-time":"2020-02-25T00:00:00Z","timestamp":1582588800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,2,25]],"date-time":"2020-02-25T00:00:00Z","timestamp":1582588800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s10817-020-09546-z","type":"journal-article","created":{"date-parts":[[2020,2,25]],"date-time":"2020-02-25T12:03:04Z","timestamp":1582632184000},"page":"611-640","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment"],"prefix":"10.1007","volume":"64","author":[{"given":"Andreas","family":"Teucke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6002-0458","authenticated-orcid":false,"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,2,25]]},"reference":[{"issue":"3","key":"9546_CR1","doi-asserted-by":"publisher","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":"9546_CR2","doi-asserted-by":"publisher","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":"9546_CR3","doi-asserted-by":"publisher","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.W., 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":"9546_CR4","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1142\/S0218213006002552","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9546_CR5","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction\u2014CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28\u2013August 2, 2003, Proceedings, Lecture Notes in Computer Science","author":"P Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) Automated Deduction\u2014CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28\u2013August 2, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2741, pp. 350\u2013364. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_32"},{"key":"9546_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-2653-9","volume-title":"Automated Model Building. Applied Logic","author":"R Caferra","year":"2004","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic, vol. 31. Springer, Berlin (2004)"},{"key":"9546_CR7","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata (2007). Release October, 12th 2007"},{"issue":"3","key":"9546_CR8","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 $$\\cal{H}_1$$ by resolution. Inf. Process. Lett. 95(3), 401\u2013408 (2005). https:\/\/doi.org\/10.1016\/j.ipl.2005.04.007","journal-title":"Inf. Process. Lett."},{"key":"9546_CR9","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0052362","volume-title":"Rewriting Techniques and Applications, 9th International Conference, RTA-98, LNCS","author":"F Jacquemard","year":"1998","unstructured":"Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in extensions of shallow equational theories. In: Nipkow, T. (ed.) Rewriting Techniques and Applications, 9th International Conference, RTA-98, LNCS, vol. 1379, pp. 76\u201390. Springer, Berlin (1998)"},{"key":"9546_CR10","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315, 2008, Proceedings, Lecture Notes in Computer Science","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iprover\u2014an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5195, pp. 292\u2013298. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"9546_CR11","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"Konstantin Korovin","year":"2013","unstructured":"Korovin, K.: Inst-Gen\u2014a modular approach to instantiation-based automated reasoning. In: Programming Logics\u2014Essays in Memory of Harald Ganzinger, pp. 239\u2013270 (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_10"},{"key":"9546_CR12","first-page":"1","volume-title":"Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, Lecture Notes in Computer Science","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 1\u201335. Springer, Berlin (2013)"},{"issue":"20","key":"9546_CR13","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. Inf. Process. Lett. 111(20), 1007\u20131013 (2011)","journal-title":"Inf. Process. Lett."},{"key":"9546_CR14","unstructured":"Seidl, H., Reu\u00df, A.: Extending $${\\cal{H}}\\_1$$-clauses with path disequalities. In: L.\u00a0Birkedal (ed.) Foundations of Software Science and Computational Structures\u201415th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24\u2013April 1, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7213, pp. 165\u2013179. Springer (2012)"},{"key":"9546_CR15","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. Lecture Notes in Computer Science","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. Lecture Notes in Computer Science, pp. 97\u2013119. Springer, Berlin (2007)"},{"key":"9546_CR16","first-page":"141","volume-title":"Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, March 26\u201329, 1996, Proceedings, Applied Logic Series,","author":"JK Slaney","year":"1996","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\u201329, 1996, Proceedings, Applied Logic Series, vol. 3, pp. 141\u2013155. Kluwer Academic Publishers, Berlin (1996)"},{"key":"9546_CR17","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-14203-1_38","volume-title":"Automated Reasoning","author":"Martin Suda","year":"2010","unstructured":"Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Automated Reasoning, 5th International Joint Conference, IJCAR 2010, LNAI, vol. 6173, pp. 441\u2013456. Springer, Edinburgh (2010)"},{"issue":"4","key":"9546_CR18","doi-asserted-by":"publisher","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. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"9546_CR19","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-29007-8_2","volume-title":"Frontiers of Combining Systems\u201412th International Symposium, FroCoS 2019, London, UK, September 4\u20136, 2019, Proceedings, Lecture Notes in Computer Science","author":"A Teucke","year":"2019","unstructured":"Teucke, A., Voigt, M., Weidenbach, C.: On the expressivity and applicability of model representation formalisms. In: Herzig, A., Popescu, A. (eds.) Frontiers of Combining Systems\u201412th International Symposium, FroCoS 2019, London, UK, September 4\u20136, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11715, pp. 22\u201339. Springer, Berlin (2019)"},{"key":"9546_CR20","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-24246-0_6","volume-title":"Frontiers of Combining Systems: 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21\u201324, 2015, Proceedings","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.) Frontiers of Combining Systems: 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21\u201324, 2015, Proceedings, pp. 85\u2013100. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_6"},{"key":"9546_CR21","unstructured":"Teucke, A., Weidenbach, C.: Ordered resolution with straight dismatching constraints. In: P.\u00a0Fontaine, S.\u00a0Schulz, J.\u00a0Urban (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, July 2nd, 2016. CEUR Workshop Proceedings, vol. 1635, pp. 95\u2013109. CEUR-WS.org (2016). http:\/\/ceur-ws.org\/Vol-1635\/paper-09.pdf"},{"key":"9546_CR22","doi-asserted-by":"crossref","unstructured":"Teucke, A., Weidenbach, C.: Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints. arXiv:1703.02837 (2017)","DOI":"10.1007\/978-3-319-63046-5_13"},{"key":"9546_CR23","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification\u201426th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201422, 2014. Proceedings, Lecture Notes in Computer Science","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification\u201426th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201422, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559, pp. 696\u2013710. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46"},{"key":"9546_CR24","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"16th International Conference on Automated Deduction, CADE-16, LNAI","author":"C Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) 16th International Conference on Automated Deduction, CADE-16, LNAI, vol. 1632, pp. 314\u2013328. Springer, Berlin (1999)"},{"key":"9546_CR25","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction\u2014CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2\u20137, 2009. Proceedings, Lecture Notes in Computer Science","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.) Automated Deduction\u2014CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2\u20137, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5663, pp. 140\u2013145. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09546-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-020-09546-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09546-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T00:18:17Z","timestamp":1614125897000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-020-09546-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,25]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["9546"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09546-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,2,25]]},"assertion":[{"value":"30 January 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}