کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6853127 | 658309 | 2016 | 25 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A formalization of programs in first-order logic with a discrete linear order
ترجمه فارسی عنوان
رسمی سازی برنامه ها در منطق مرتبه اول با یک دستور خطی گسسته
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
معانی برنامه، استدلال در مورد برنامه ها، منطق اولویت،
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
چکیده انگلیسی
We consider the problem of representing and reasoning about computer programs, and propose a translation from a core procedural iterative programming language to first-order logic with quantification over the domain of natural numbers that includes the usual successor function and the “less than” linear order, essentially a first-order logic with a discrete linear order. Unlike Hoare's logic, our approach does not rely on loop invariants. Unlike the typical temporal logic specification of a program, our translation does not require a transition system model of the program, and is compositional on the structures of the program. Some non-trivial examples are given to show the effectiveness of our translation for proving properties of programs.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Artificial Intelligence - Volume 235, June 2016, Pages 1-25
Journal: Artificial Intelligence - Volume 235, June 2016, Pages 1-25
نویسندگان
Fangzhen Lin,