کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6424846 | 1633492 | 2011 | 10 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Unification in linear temporal logic LTL
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
We prove that a propositional Linear Temporal Logic with Until and Next (LTL) has unitary unification. Moreover, for every unifiable in LTL formula A there is a most general projective unifier, corresponding to some projective formula B, such that A is derivable from B in LTL. On the other hand, it can be shown that not every open and unifiable in LTL formula is projective. We also present an algorithm for constructing a most general unifier.
⺠We study unification problem for linear temporal logic LTL. ⺠We prove that every unifiable in LTL formula has a most general unifier. ⺠We also construct an algorithm building most general unifiers. ⺠This algorithm solves the unification problem in LTL.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 162, Issue 12, December 2011, Pages 991-1000
Journal: Annals of Pure and Applied Logic - Volume 162, Issue 12, December 2011, Pages 991-1000
نویسندگان
Sergey Babenyshev, Vladimir Rybakov,