2021/04/23 by Martin Raška, Raška, Martin, Štěpán Starosta +1
Computer Science · #03B35 #68R15 #68V15 #68V20 #Algorithms and Data Compression #D.2.4 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Natural Language Processing Techniques #Rough Sets and Fuzzy Logic #Semantic Web and Ontologies #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2104.11622
openalex publication_date 2021/04/23 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
Many facts possess symmetrical counterparts that often require a separate\nformal proof, depending on the nature of the involved symmetry. We introduce a\nmethod in Isabelle/HOL which produces such a symmetrical fact for the list\ndatatype and the symmetry induced by the list reversal mapping. The method is\nimplemented as an attribute and its result is based on user-declared symmetry\nrules. Besides general rules, we provide rules that are aimed to be applied in\nthe domain of Combinatorics on Words.\n