-
sat solving for termination proofs with recursive path orders and dependency pairs
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 805
- تعداد پرسش و پاسخ ها: 0
- شماره تماس دبیرخانه رویداد: -
this paper introduces a propositional encoding for recursive path orders (rpo), in connection with dependency pairs. hence, we capture in a uniform setting all common instances of rpo, i.e., lexicographic path orders (lpo), multiset path orders (mpo), and lexicographic path orders with status (lpos). this facilitates the application of sat solvers for termination analysis of term rewrite systems (trss). we address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by sat solving: (a) the lexicographic comparison w.r.t. a permutation of the arguments; (b) the multiset extension of a base order; (c) the combined search for a path order together with an argument filter to orient a set of inequalities; and (d) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-called usable rules). we have implemented our contributions in the termination prover aprove. extensive experiments show that by our encoding and the application of sat solvers one obtains speedups in orders of magnitude as well as increased termination proving power.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
آلودگی جیوه و آرسنیک در رسوبات سطحی تالاب انزلی
-
ارتشاء آفتی برای اخلاق حرفه ای
-
تاثیر نگهداشت وجه نقد مازاد بر حاکمیت شرکتی و عملکرد شرکت ها در شرایط بحران و عدم بحران مالی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
تأثیر انحراف و بی ثباتی نرخ ارز بر صادرات غیرنفتی در ایران: رویکرد ناترکس
-
removal of uranium(vi) from aqueous solutions by magnetic mg–al layered double hydroxide intercalated with citrate: kinetic and thermodynamic investigation
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
نقش فرهنگ سازمانی در مدیریت کیفیت دانشگاه (مورد مطالعه: دانشگاه آزاد اسلامی واحد شوشتر)
-
بررسی تاثیر دستکاری جریان نقد عملیاتی برخطر سقوط قیمت سهام شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
مدل سازی قیمت گذاری آپارتمان های مسکونی در شهر تهران با استفاده از سیستم پویا
-
evaluation of forta fibers performance in hot asphalt mixture against concrete cover
-
designing a transformational leadership model for the employees of health and treatment centers in tehran utilizing the theme analysis method
سوال خود را در مورد این مقاله مطرح نمایید :