On the scope of static checking in definitional languages
Boleslaw Karol Szymanski, Noah S. Prywes, Evan Lock, Amir Pnueli · 1984
The paper concerns the use in software development of a class of very high level languages characterized as definitional, where a specification of a program consists of assertions expressed as conditional equations. As compared to logic programming, where assertion are expressed in the form of Horn clauses, definitional languages are more amenable to efficient compilation. Also, use of equations is a natural way of expressing mathematical models in science, engineering and economics, where computer simulation of such models is often required. Finally, definitional languages are well suited for programming dataflow machines, another important building block in a Fifth Generation Project. Thus, in many applications definitional languages are preferred choice for programming new generation computers.