{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:48:18Z","timestamp":1776509298626,"version":"3.51.2"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_6","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:40:17Z","timestamp":1759844417000},"page":"91-109","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Supporting Maintenance of Formal Mathematics with Similarity Search"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9418-1580","authenticated-orcid":false,"given":"Fabian","family":"Huch","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Adams, M.: Refactoring Proofs with Tactician. In: Software Engineering and Formal Methods. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-49224-6_6","DOI":"10.1007\/978-3-662-49224-6_6"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Alkassar, E., Hillebrand, M.A., Leinenbach, D.C., Schirmer, N.W., Starostin, A., Tsyban, A.: Balancing the Load. Journal of Automated Reasoning (2009). https:\/\/doi.org\/10.1007\/s10817-009-9123-z","DOI":"10.1007\/s10817-009-9123-z"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Aspinall, D., Kaliszyk, C.: Towards Formal Proof Metrics. In: Fundamental Approaches to Software Engineering. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49665-7_19","DOI":"10.1007\/978-3-662-49665-7_19"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Baumgartner, A., Kutsia, T., Levy, J., Villaret, M.: A Variant of Higher-Order Anti-Unification. In: Rewriting Techniques and Applications. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2013). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.113","DOI":"10.4230\/LIPIcs.RTA.2013.113"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Baumgartner, A., Kutsia, T., Levy, J., Villaret, M.: Higher-Order Pattern Anti-Unification in Linear Time. Journal of Automated Reasoning (2017). https:\/\/doi.org\/10.1007\/s10817-016-9383-3","DOI":"10.1007\/s10817-016-9383-3"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and Experiences in Managing Large-Scale Proofs. In: Intelligent Computer Mathematics. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31374-5_3","DOI":"10.1007\/978-3-642-31374-5_3"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Brown, C., Thompson, S.: Clone detection and elimination for Haskell. In: Partial Evaluation and Program Manipulation. ACM (2010). https:\/\/doi.org\/10.1145\/1706356.1706378","DOI":"10.1145\/1706356.1706378"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Cerna, D.M., Buran, M.: One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus. ACM Trans. Comput. Logic (2024). https:\/\/doi.org\/10.1145\/3654798","DOI":"10.1145\/3654798"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Cerna, D.M., Kutsia, T.: A Generic Framework for Higher-Order Generalizations. In: Formal Structures for Computation and Deduction. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.10","DOI":"10.4230\/LIPIcs.FSCD.2019.10"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Chodarev, S., Pietrikov\u00e1, E., Koll\u00e1r, J.: Haskell clone detection using pattern comparing algorithm. In: Engineering of Modern Electric Systems. IEEE (2015). https:\/\/doi.org\/10.1109\/EMES.2015.7158423","DOI":"10.1109\/EMES.2015.7158423"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Cohen, S.: Indexing for subtree similarity-search using edit distance. In: Management of Data. ACM (2013). https:\/\/doi.org\/10.1145\/2463676.2463716","DOI":"10.1145\/2463676.2463716"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Dietrich, D., Whiteside, I., Aspinall, D.: Polar: A Framework for Proof Refactoring. In: Logic for Programming, Artificial Intelligence, and Reasoning. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_52","DOI":"10.1007\/978-3-642-45221-5_52"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"van Doorn, F., Ebner, G., Lewis, R.Y.: Maintaining a Library of Formal Mathematics. In: Intelligent Computer Mathematics. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_16","DOI":"10.1007\/978-3-030-53518-6_16"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Du, D., Pardalos, P., Hu, X., Wu, W.: Introduction to Combinatorial Optimization. Springer, 1 edn. (2022). https:\/\/doi.org\/10.1007\/978-3-031-10596-8","DOI":"10.1007\/978-3-031-10596-8"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Fortunato, S., Hric, D.: Community detection in networks: A user guide. Physics Reports (2016). https:\/\/doi.org\/10.1016\/j.physrep.2016.09.002","DOI":"10.1016\/j.physrep.2016.09.002"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Gauthier, T., Kaliszyk, C.: Matching Concepts across HOL Libraries. In: Intelligent Computer Mathematics. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_20","DOI":"10.1007\/978-3-319-08434-3_20"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Gauthier, T., Kaliszyk, C.: Aligning concepts across proof assistant libraries. Journal of Symbolic Computation (2019). https:\/\/doi.org\/10.1016\/j.jsc.2018.04.005","DOI":"10.1016\/j.jsc.2018.04.005"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Ghanbari, A.: Automatic Goal Clone Detection in Rocq. In: 39th European Conference on Object-Oriented Programming (ECOOP 2025). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2025.12","DOI":"10.4230\/LIPIcs.ECOOP.2025.12"},{"key":"6_CR19","unstructured":"Ghanouchi, S.: Code Clone Detection in Isabelle Using Token Stream Similarity. Bachelor\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2023)"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Huch, F.: Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs. In: Intelligent Computer Mathematics. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_10","DOI":"10.1007\/978-3-031-16681-5_10"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Huch, F., Stathopoulos, Y.: Formalization Quality in Isabelle. In: Intelligent Computer Mathematics. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-42753-4_10","DOI":"10.1007\/978-3-031-42753-4_10"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Jiang, L., Misherghi, G., Su, Z., Glondu, S.: DECKARD: Scalable and Accurate Tree-Based Detection of Code Clones. In: Software Engineering. IEEE (2007). https:\/\/doi.org\/10.1109\/ICSE.2007.30","DOI":"10.1109\/ICSE.2007.30"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Li, H., Thompson, S.: Similar Code Detection and Elimination for Erlang Programs. In: Practical Aspects of Declarative Languages. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-11503-5_10","DOI":"10.1007\/978-3-642-11503-5_10"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Megdiche, Y., Huch, F., Stevens, L.: A Linter for Isabelle: Implementation and Evaluation (2022). https:\/\/doi.org\/10.48550\/arXiv.2207.10424, Isabelle Workshop","DOI":"10.48550\/arXiv.2207.10424"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"M\u00fcller, D., Gauthier, T., Kaliszyk, C., Kohlhase, M., Rabe, F.: Classification of Alignments Between Concepts of Formal Mathematical Systems. In: Intelligent Computer Mathematics. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_7","DOI":"10.1007\/978-3-319-62075-6_7"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Pan, W.F., Jiang, B., Li, B.: Refactoring Software Packages via Community Detection in Complex Software Networks. International Journal of Automation and Computing (2013). https:\/\/doi.org\/10.1007\/s11633-013-0708-y","DOI":"10.1007\/s11633-013-0708-y"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Pan, W., Li, B., Ma, Y., Liu, J., Qin, Y.: Class structure refactoring of object-oriented softwares using community detection in dependency networks. Frontiers of Computer Science in China (2009). https:\/\/doi.org\/10.1007\/s11704-009-0054-y","DOI":"10.1007\/s11704-009-0054-y"},{"key":"6_CR28","unstructured":"Ringer, T.: Proof Repair. Ph.D. thesis, University of Washington (2021)"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Ringer, T., Porter, R., Yazdani, N., Leo, J., Grossman, D.: Proof repair across type equivalences. In: Programming Language Design and Implementation. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454033","DOI":"10.1145\/3453483.3454033"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Ringer, T., Yazdani, N., Leo, J., Grossman, D.: Adapting proof automation to adapt proofs. In: Certified Programs and Proofs. ACM (2018). https:\/\/doi.org\/10.1145\/3167094","DOI":"10.1145\/3167094"},{"key":"6_CR31","unstructured":"Sch\u00e4fer, M.: Community Detection on the Isabelle Dependency Graph. Bachelor\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2023)"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Vanhoof, W., Yernaux, G.: Generalization-Driven Semantic Clone Detection in CLP. In: Logic-Based Program Synthesis and Transformation. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45260-5_14","DOI":"10.1007\/978-3-030-45260-5_14"},{"key":"6_CR33","unstructured":"Vinan, D., Hupel, L.: Clone Detection in Isabelle Theories (2016), Isabelle Workshop"},{"key":"6_CR34","doi-asserted-by":"publisher","unstructured":"\u0160ubelj, L., Bajec, M.: Software systems through complex networks science: review, analysis and applications. In: Software Mining. ACM (2012). https:\/\/doi.org\/10.1145\/2384416.2384418","DOI":"10.1145\/2384416.2384418"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"Wang, J., Li, G., Fe, J.: Fast-join: An efficient method for fuzzy token matching based string similarity join. In: Data Engineering. IEEE (2011). https:\/\/doi.org\/10.1109\/ICDE.2011.5767865","DOI":"10.1109\/ICDE.2011.5767865"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards Formal Proof Script Refactoring. In: Intelligent Computer Mathematics. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_18","DOI":"10.1007\/978-3-642-22673-1_18"},{"key":"6_CR37","unstructured":"Wibergh, K.: Automatic refactoring for Agda. Master\u2019s thesis, University of Gothenburg (2019)"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"Zakeri-Nasrabadi, M., Parsa, S., Ramezani, M., Roy, C., Ekhtiarzadeh, M.: A systematic literature review on source code similarity measurement and clone detection: Techniques, applications, and challenges. Journal of Systems and Software (2023). https:\/\/doi.org\/10.1016\/j.jss.2023.111796","DOI":"10.1016\/j.jss.2023.111796"},{"key":"6_CR39","doi-asserted-by":"publisher","unstructured":"Zhang, K.: A constrained edit distance between unordered labeled trees. Algorithmica (1996). https:\/\/doi.org\/10.1007\/BF01975866","DOI":"10.1007\/BF01975866"},{"key":"6_CR40","doi-asserted-by":"publisher","unstructured":"\u0160ubelj, L., Bajec, M.: Community structure of complex software systems: Analysis and applications. Physica A: Statistical Mechanics and its Applications (2011). https:\/\/doi.org\/10.1016\/j.physa.2011.03.036","DOI":"10.1016\/j.physa.2011.03.036"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:21:46Z","timestamp":1776507706000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032070203","9783032070210"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"8 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}