Automated theorem proving: theory and practice

با شروع قرن بیست و یکم، قدرت ابزار و شریک جادویی جدید ما، رایانه، با سرعت شگفت انگیزی در حال افزایش است. رایانه‌هایی که میلیاردها عملیات در ثانیه انجام می‌دهند اکنون رایج هستند. چند پردازنده با هزاران کامپیوتر کوچک - نسبتاً کم! -اکنون می تواند محاسبات موازی انجام دهد و مسائلی را در چند ثانیه حل کند که فقط چند سال پیش روزها یا ماه ها طول می کشید. برنامه های شطرنج بازی با بهترین بازیکنان جهان برابر است. Deep Blue از IBM چندین سال پیش در مسابقه ای قهرمان جهان گری کاسپاروف را شکست داد. انتظار می رود رایانه ها به طور فزاینده ای باهوش تر باشند، استدلال کنند، بتوانند از حقایق داده شده نتیجه گیری کنند، یا به طور انتزاعی، قضایای موضوع این کتاب را اثبات کنند. به طور خاص، این کتاب در مورد دو برنامه اثبات قضیه، THEO و HERBY است. چهار فصل اول حاوی مطالب مقدماتی در مورد اثبات قضیه خودکار و دو برنامه است. این شامل مطالبی در مورد زبان مورد استفاده برای بیان قضایا، محموله‌های محمول و قواعد استنتاج است. این همچنین شامل توضیحات برنامه سوم همراه با این بسته به نام COMPILE است. همانطور که در فصل 3 توضیح داده شد، COMPILE عبارات حساب محمول را همانطور که توسط HERBY و THEO مورد نیاز است، به شکل بند تبدیل می کند. فصل 5 مبانی نظری اثبات قضیه درخت معنایی را که توسط HERBY انجام شده است، ارائه می کند. فصل 6 مبانی نظری قضیه حل و فصل ابطال اثبات شده توسط THEO را ارائه می کند. فصل 7 و 8 HERBY و نحوه استفاده از آن را شرح می دهد.

As the 21st century begins, the power of our magical new tool and partner, the computer, is increasing at an astonishing rate. Computers that perform billions of operations per second are now commonplace. Multiprocessors with thousands of little computers - relatively little! -can now carry out parallel computations and solve problems in seconds that only a few years ago took days or months. Chess-playing programs are on an even footing with the world's best players. IBM's Deep Blue defeated world champion Garry Kasparov in a match several years ago. Increasingly computers are expected to be more intelligent, to reason, to be able to draw conclusions from given facts, or abstractly, to prove theorems-the subject of this book. Specifically, this book is about two theorem-proving programs, THEO and HERBY. The first four chapters contain introductory material about automated theorem proving and the two programs. This includes material on the language used to express theorems, predicate calculus, and the rules of inference. This also includes a description of a third program included with this package, called COMPILE. As described in Chapter 3, COMPILE transforms predicate calculus expressions into clause form as required by HERBY and THEO. Chapter 5 presents the theoretical foundations of seman­ tic tree theorem proving as performed by HERBY. Chapter 6 presents the theoretical foundations of resolution-refutation theorem proving as per­ formed by THEO. Chapters 7 and 8 describe HERBY and how to use it.