Computer Program Synthesis Methodologies: Proceedings of the NATO Advanced Study Institute held at Bonas, France, September 28–October 10, 1981

عملیات قدرتمند بر روی آنها. گام اولیه در این مسیر، توسعه APl بود، و نمونه‌های جدیدتر SETl است که کاربر را قادر می‌سازد بر حسب موجودیت‌های ریاضی مانند مجموعه‌ها و BDl کدنویسی کند که به کاربر، احتمالاً یک تاجر، اجازه می‌دهد تا یک محاسبات را مشخص کند. اصطلاحات یک سری اشکال جدولی و یک سری مسیرهای پردازشی که داده ها از طریق آنها جریان می یابد. طراحی و اجرای چنین زبان هایی در فصل هایی توسط P. GOLDBERG مورد بررسی قرار گرفته است. گسترش دیگری برای روش‌های سنتی توسط سیستم‌هایی که برای کنترل خودکار تصمیم‌های کنترل جریان در سطح پایین طراحی شده‌اند ممکن می‌شود. تمام زبان های سطح بالاتر بالا این کار را به طور ضمنی با عملگرهای داخلی خود انجام می دهند. PROLOG زبانی است که این کار را با مکانیزم اثبات قضیه انجام می دهد که عمدتاً از یکسان سازی و عقب نشینی استفاده می کند. برنامه نویس مسئله ای را که باید با مجموعه ای از گزاره های منطقی رسمی از جمله یک قضیه برای اثبات حل شود، مشخص می کند. سیستم اثبات قضیه راهی برای ترکیب بدیهیات برای اثبات قضیه پیدا می کند و در این فرآیند، محاسبه مورد نظر را تکمیل می کند. H. GALLAIRE فصلی را ارائه کرده است که در آن PROLOG مثال‌های زیادی از استفاده از آن ارائه می‌کند.

powerful operations on them. An early step in this direction was the development of APl, and more recent examples have been SETl which enables a user to code in terms of mathematical enti­ ties such as sets and BDl which allows a user, presumably a businessman, to specify a computation in terms of a series of tabular forms and a series of processing paths through which data flows. The design and implementation of such languages are examined in chapters by P. GOLDBERG. Another extension to traditional methods is made possible by systems designed to automatically handle low level flow-of­ control decisions. All the above higher level languages do this implicitly with their built in operators. PROLOG is a language which does this with a theorem proving mechanism employing primarily unification and backtracking. The programmer specifies the problem to be solved with a set of formal logic statements including a theorem to be proved. The theorem proving system finds a way to combine the axioms to prove the theorem, and in the process, it completes the desired calculation. H. GAllAIRE has contributed a chapter describing PROLOG giving many examples of its usage.