Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version)

Naoki Nishida, Misaki Kojima, Yuto Nakamura

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 divide…