Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Journal Article

A Higher-order Interpretation of Deductive Tableau


Ayari,  Abdelwaheb
Programming Logics, MPI for Informatics, Max Planck Society;


Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Ayari, A., & Basin, D. A. (2001). A Higher-order Interpretation of Deductive Tableau. Journal of Symbolic Computation, 31(5), 487-520.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-31D6-A
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.