• as linear CHC: an approach called property-directed reachability proposed as a solver of finite model-checking that corresponds to linear CHCs over finite data domain, also applied to non linear CHCs (GPDR)
• Spacer is based on several new ideas, but the key to refutational completeness is a technique called model-based projection. It is used to divide the set of local candidatesof counterexamples into a finite number of classes, and the finiteness of the classes allows an exhaustive search for candidates of global counterexamples in a finite number of steps.
• the refutational completeness of spacer seems to be a matter of discussion? there exists a refutationally complete variant