Knowledge and Reasoning in Program Synthesis
Knowledge and Reasoning in Program Synthesis
复制标题
程序综合中的知识与推理
DOI：
--
复制
发表时间：
1974
期刊：
影响因子：
--
通讯作者：
Z. Manna
中科院分区：
文献类型：
--
作者：
Z. Manna
摘要 程序综合是根据给定的规范构建计算机程序。自动程序合成系统必须将推理和编程能力与有关程序主题的大量知识结合起来。这种能力和知识必须在程序上（通过程序）和结构上（通过表示的选择）体现出来。我们描述了投影综合系统的一些推理和编程功能。特别注意在正在构建的程序中引入条件测试、循环和具有副作用的指令。在许多情况下，同时满足多个相互作用的目标的能力被证明是很重要的。人们发现，修改现有程序来解决有些不同的问题是一种有效的方法。我们通过对多个模式匹配程序的合成进行手动模拟来说明这些概念。其中一些技术已经实现，一些正在实现过程中，而另一些技术似乎相当于人工智能中众所周知的未解决问题。
Abstract Program synthesis is the construction of a computer program from given specifications. An automatic program synthesis system must combine reasoning and programming ability with a good deal of knowledge about the subject matter of the program. This ability and knowledge must be manifested both procedurally (by programs) and structurally (by choice of representation). We describe some of the reasoning and programming capabilities of a projected synthesis system. Special attention is paid to the introduction of conditional tests, loops, and instructions with side effects in the program being constructed. The ability to satisfy several interacting goals simultaneously proves to be important in many contexts. The modification of an already existing program to solve a somewhat different problem has been found to be a powerful approach. We illustrate these concepts with hand simulations of the synthesis of a number of pattern-matching programs. Some of these techniques have already been implemented, some are in the course of implementation, while others seem equivalent to well-known unsolved problems in artificial intelligence.