Justification of the structural synthesis of programs

AbstractWe present a constructive description of the automatic program synthesis method used in the PRIZ programming system. We give a justification of the method by proving the completeness of its inference rules for the class of constructive theories, and we present rules for transforming any intuitionistic propositional formula into a form suitable for these inference rules