2025/07/05 by Naoki Nishida, Nishida, Naoki, Misaki Kojima +3
Computer Science · #Advanced Database Systems and Queries #Algorithms and Data Compression #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2507.04080
openalex publication_date 2025/07/05 · openalex created_date 2025/10/14 · openalex updated_date 2026/07/28
Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the dividend pattern and the divisor pattern. A complement of a pattern is a pattern set, the ground constructor instances of which comprise the complement of the ground constructor instances of the former pattern. Given finitely many unconstrained linear patterns, using a difference operator over linear patterns, a complement algorithm returns a finite set of linear patterns as a complement of the given patterns. In this paper, we extend the difference operator and complement algorithm to constrained linear patterns used in logically constrained term rewrite systems (LCTRSs, for short) that have no user-defined constructor term with a sort for built-in values. Then, as for left-linear term rewrite systems, using the complement algorithm, we show that quasi-reducibility is decidable for such LCTRSs with decidable built-in theories. For the single use of the difference operator over constrained patterns, only divisor patterns are required to be linear.