کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6424846 1633492 2011 10 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Unification in linear temporal logic LTL
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
پیش نمایش صفحه اول مقاله
Unification in linear temporal logic LTL
چکیده انگلیسی

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
نویسندگان
, ,