Automated Deduction — A Basis for Applications: Volume II: Systems and Implementation Techniques

1. مفاهیم اساسی اثبات قضیه تعاملی اثبات قضیه تعاملی در نهایت به ساخت ابزارهای استدلالی قدرتمندی می‌پردازد که به ما (دانشمندان رایانه) اجازه می‌دهند چیزهایی را ثابت کنیم که بدون ابزار نمی‌توانیم اثبات کنیم، و ابزارها نمی‌توانند بدون ما ثابت کنند. تعامل معمولاً مورد نیاز است، برای مثال، برای هدایت و کنترل استدلال، حدس و گمان یا تعمیم لم های راهبردی، و گاهی اوقات صرفاً به این دلیل که حدسی که باید اثبات شود صادق نیست. برای مثال، در تأیید نرم‌افزار، نسخه‌های صحیح مشخصات و برنامه‌ها معمولاً تنها پس از تعدادی تلاش برای اثبات ناموفق و تصحیح خطاهای بعدی به دست می‌آیند. اثبات‌کننده‌های قضیه تعاملی مختلف ممکن است در واقع کاملاً متفاوت به نظر برسند: آنها ممکن است از منطق‌های متفاوتی پشتیبانی کنند (نظام اول یا بالاتر، منطق برنامه‌ها، نظریه نوع و غیره)، ممکن است ابزارهای عمومی یا با هدف خاص باشند، یا ممکن است به برنامه‌های مختلف تبدیل شوند. . با این وجود، آنها مفاهیم و پارادایم های مشترکی دارند (مانند طراحی معماری، تاکتیک ها، استدلال تاکتیکی و غیره). هدف این فصل توصیف مفاهیم رایج، اصول طراحی و الزامات اساسی اثبات‌کننده‌های قضیه تعاملی و کشف پهنای باند تغییرات است. وجود یک «شخص در حلقه»، به شدت بر طراحی ابزار اثبات تأثیر می‌گذارد: اثبات‌ها باید قابل درک باقی بمانند، - قوانین اثبات باید سطح بالا و انسان محور باشند، - ارائه اثبات مداوم و تجسم بسیار مهم می‌شود.

1. BASIC CONCEPTS OF INTERACTIVE THEOREM PROVING Interactive Theorem Proving ultimately aims at the construction of powerful reasoning tools that let us (computer scientists) prove things we cannot prove without the tools, and the tools cannot prove without us. Interaction typi­ cally is needed, for example, to direct and control the reasoning, to speculate or generalize strategic lemmas, and sometimes simply because the conjec­ ture to be proved does not hold. In software verification, for example, correct versions of specifications and programs typically are obtained only after a number of failed proof attempts and subsequent error corrections. Different interactive theorem provers may actually look quite different: They may support different logics (first-or higher-order, logics of programs, type theory etc.), may be generic or special-purpose tools, or may be tar­ geted to different applications. Nevertheless, they share common concepts and paradigms (e.g. architectural design, tactics, tactical reasoning etc.). The aim of this chapter is to describe the common concepts, design principles, and basic requirements of interactive theorem provers, and to explore the band­ width of variations. Having a 'person in the loop', strongly influences the design of the proof tool: proofs must remain comprehensible, - proof rules must be high-level and human-oriented, - persistent proof presentation and visualization becomes very important.