کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422363 685074 2008 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Maude as a Platform for Designing and Implementing Deep Inference Systems
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Maude as a Platform for Designing and Implementing Deep Inference Systems
چکیده انگلیسی

Deep inference is a proof theoretical methodology that generalizes the traditional notion of inference in the sequent calculus: in contrast to the sequent calculus, the deductive systems with deep inference do not rely on the notion of main connective, and permit the application of the inference rules at any depth inside logical expressions, in a way which resembles the application of term rewriting rules. Deep inference provides a richer combinatoric analysis of proofs for different logics. In particular, construction of exponentially shorter proofs becomes possible. In this paper, aiming at the development of computation as proof search tools, we propose the Maude language as a means for designing and implementing different deep inference deductive systems and proof strategies that work on these systems. We give Maude implementations of deep inference systems together with an implementation that simulates sequent calculus proofs to serve as a benchmark. We demonstrate these ideas on classical logic, and argue that they can be analogously carried to other deep inference systems for other logics, as well as sequent calculus systems.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 219, 20 November 2008, Pages 35-50