Automatically Proving and Disproving Feasibility Conditions

Abstract

In the realm of term rewriting, given terms s and t, a reachability condition s→∗t is called feasible if there is a substitution σ such that σ(s) rewrites into σ(t) 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.