Title :
Mechanical synthesis of a unification algorithm in PowerEpsilon
Author :
Zhu, Ming-Yuan ; Mo, Xiao-Bai
Author_Institution :
Artificial Intelligence Lab., Beijing Inst. of Syst. Eng., China
Abstract :
Programming in constructive type theory corresponds to theorem proving in mathematics: the specification plays the role of the proposition to be proved and the program is obtained from the proof. We present a proof development system called PowerEpsilon, based on a constructive type theory which can be used as a formal program development system for actually deriving a program from a specification. The synthesis of a unification algorithm is presented to show the power of the system
Keywords :
formal specification; programming theory; theorem proving; type theory; PowerEpsilon; constructive type theory; formal program development system; mechanical synthesis; programming; proof development system; specification; unification algorithm; Logic programming; Production; Reactive power;
Conference_Titel :
Computer Software and Applications Conference, 1995. COMPSAC 95. Proceedings., Nineteenth Annual International
Conference_Location :
Dallas, TX
Print_ISBN :
0-8186-7119-X
DOI :
10.1109/CMPSAC.1995.524758
