Use of logical models for proving infeasibility in term rewriting

摘要

Given a (Conditional) Rewrite System R and terms s and t, we consider the following problem: is there a substitution a instantiating the variables in s and t such that the reachability test sigma(s) - *(R) sigma(t) succeeds? If such a substitution does not exist, we say that the problem is infeasible; otherwise, we call it feasible. Similarly, we can consider reducibility, involving a single rewriting step. In term rewriting, a number of important problems involve such infeasibility tests (e.g., confluence and termination analysis). We show how to recast infeasibility tests into the problem of finding a model of a set of (first-order) sentences representing the operational semantics of R together with some additional sentences representing the considered property which is formulated as an infeasibility test. (C) 2018 Elsevier B.V. All rights reserved.