Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874169 | Information Processing Letters | 2018 | 6 Pages |
Abstract
Given a (Conditional) Rewrite System R and terms s and t, we consider the following problem: is there a substitution Ï instantiating the variables in s and t such that the reachability testÏ(s)âRâÏ(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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Salvador Lucas, Raúl Gutiérrez,