@article{AyariBasin01,
  author =       "Abdelwaheb Ayari and David Basin",
  title =        "A Higher-order Interpretation of Deductive Tableau",
  journal =      "Journal of Symbolic Computation",
  volume =       "31",
  number =       "5",
  pages =        "487--520",
  day =          "1",
  month =        "May",
  year =         "2001",
  abstract = {
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.  }
}