کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6874169 1441026 2018 6 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
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 σ 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.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information Processing Letters - Volume 136, August 2018, Pages 90-95
نویسندگان
, ,