کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423637 685267 2008 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Regular Strategies as Proof Tactics for CIRC
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Regular Strategies as Proof Tactics for CIRC
چکیده انگلیسی

CIRC is an automated circular coinductive prover implemented as an extension of Maude. The main engine of CIRC consists of a set of rewriting rules implementing the circularity principle. The power of the prover can be increased by adding new capabilities implemented also by rewriting rules. In this paper we prove the correctness of the coinductive prover and show how rewriting strategies, expressed as regular expressions, can be used for specifying proof tactics for CIRC. We illustrate the strength of the method by defining a proof tactic combining the circular coinduction with a particular form of simplification for proving the equivalence of context-free processes.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 204, 4 April 2008, Pages 83-98