Automatically Proving and Disproving Feasibility Conditions

In the realm of term rewriting, given terms s and t, a reachability condition [Formula: see text] is called feasible if there is a substitution [Formula: see text] such that [Formula: see text] rewrites into [Formula: see text] in zero or more steps; otherwise, it is called infeasible. Checking infeasibility of (sequences of) reachability conditions is important in the analysis of computational properties of rewrite systems like confluence or (operational) termination. In this paper, we generalize this notion of feasibility to arbitrary n-ary relations on terms defined by first-order theories. In this way, properties of computational systems whose operational semantics can be given as a first-order theory can be investigated. We introduce a framework for proving feasibility/infeasibility, and a new tool, infChecker, which implements it.