非表示:
キーワード:
-
要旨:
The Deductive Tableau of Manna and Waldinger is a formal system with
an associated methodology for synthesizing functional programs by
existence proofs in classical first-order theories. We reinterpret
the formal system in a setting that is higher-order in two respects:
higher-order logic is used to formalize a theory of functional
programs and higher-order resolution is used to synthesize programs
during proof. Their synthesis methodology can be applied in our
setting as well as new methodologies that take advantage of these
higher-order features.
The reinterpretation gives us a framework for directly formalizing
and implementing the Deductive Tableau system in standard theorem
provers that support the kinds of higher-order reasoning listed
above. We demonstrate this, as well as a new development
methodology, within a conservative extension of higher-order logic
in the Isabelle system. We report too on a case-study in synthesizing
sorting programs.
