Canonical Equational Proofs

معادلات در بسیاری از کاربردهای کامپیوتری مانند محاسبات نمادین، برنامه نویسی تابعی، مشخصات نوع داده انتزاعی، تأیید برنامه، ترکیب برنامه، و اثبات قضیه خودکار رخ می دهند. سیستم‌های بازنویسی معادلات هدایت‌شده‌ای هستند که برای محاسبه با جایگزین کردن زیرمجموعه‌های یک فرمول معین با عبارت‌های مساوی استفاده می‌شوند تا زمانی که ساده‌ترین شکل ممکن به نام شکل عادی به دست آید. تئوری بازنویسی با محاسبه اشکال عادی سروکار دارد. ما استفاده از تکنیک های بازنویسی را برای استدلال در مورد معادلات مطالعه خواهیم کرد. برای مثال، استدلال در مورد معادلات ممکن است مستلزم تصمیم گیری در مورد اینکه آیا یک معادله نتیجه منطقی مجموعه معینی از بدیهیات معادله است یا خیر. سیستم‌های بازنویسی همگرا آن‌هایی هستند که فرآیند بازنویسی، فرم‌های معمولی منحصربه‌فرد را برای آنها تعیین می‌کند. آنها را می توان به عنوان برنامه های کاربردی غیر قطعی در نظر گرفت و رویه های تصمیم گیری کارآمد معقولی را برای تئوری های معادله زیربنایی ارائه می کند. روش تکمیل Knuth-Bendix ابزاری برای آزمایش همگرایی فراهم می‌کند و اغلب می‌تواند برای ساختن سیستم‌های بازنویسی همگرا از سیستم‌های غیر همگرا استفاده شود. ما یک چارچوب اثبات-نظری برای مطالعه تکمیل و روش‌های اثبات مبتنی بر بازنویسی مرتبط ایجاد می‌کنیم. ما اثبات‌کننده‌های قضیه را به‌عنوان رویه‌های تبدیل اثبات می‌بینیم، تا ویژگی‌های اساسی آنها را به‌عنوان قضایای عادی‌سازی اثبات بیان کنیم.

Equations occur in many computer applications, such as symbolic compu­ tation, functional programming, abstract data type specifications, program verification, program synthesis, and automated theorem proving. Rewrite systems are directed equations used to compute by replacing subterms in a given formula by equal terms until a simplest form possible, called a normal form, is obtained. The theory of rewriting is concerned with the compu­ tation of normal forms. We shall study the use of rewrite techniques for reasoning about equations. Reasoning about equations may, for instance, involve deciding whether an equation is a logical consequence of a given set of equational axioms. Convergent rewrite systems are those for which the rewriting process de­ fines unique normal forms. They can be thought of as non-deterministic functional programs and provide reasonably efficient decision procedures for the underlying equational theories. The Knuth-Bendix completion method provides a means of testing for convergence and can often be used to con­ struct convergent rewrite systems from non-convergent ones. We develop a proof-theoretic framework for studying completion and related rewrite­ based proof procedures. We shall view theorem provers as proof transformation procedures, so as to express their essential properties as proof normalization theorems.