Meta-Amphion: Scaling up High-Assurance Deductive Program Synthesis
Steve Roach, Recom Technologies, J. Van Baalen, Michael Lowry · 1997
Amphion is a domain-independent program-synthesis system. It is specialized to specific applications through the creation of an operational domain theory. The Meta-Amphion system is being developed to empower domain experts to develop and maintain their own Amphion applications. Operationalization, a technology for automatically transforming declarative domain theories into efficient, domain-specific program synthesis systems, is described here. A prototype of the system has been implemented in TOPS, Theory Operationalization for Program Synthesis. Sets of axioms in the domain theory are replaced by specialized procedures. TOPS uses partial deduction to augment the procedure with the capability to construct ground terms for deductive synthesis. The procedures are automatically interfaced to a resolution theorem prover. Answers to deductive synthesis problem specifications can be generated using procedures synthesized by TOPS if and only if they can be generated without using the proce...