Abstract:

A Higher-order Interpretation of Deductive Tableau

Abdelwaheb Ayari and David Basin


The Deductive Tableau of Manna and Waldinger is a formal system withan associated methodology for 
synthesizing functional programs byexistence proofs in classical first-order theories. We reinterpretthe formal 
system in a setting that is higher-order in two respects:higher-order logic is used to formalize a theory of 
functionalprograms and higher-order resolution is used to synthesize programsduring proof. Their synthesis 
methodology can be applied in oursetting as well as new methodologies that take advantage of thesehigher-order 
features.The reinterpretation gives us a framework for directly formalizingand implementing the Deductive 
Tableau system in standard theoremprovers that support the kinds of higher-order reasoning listedabove. We 
demonstrate this, as well as a new developmentmethodology, within a conservative extension of higher-order 
logicin the Isabelle system. We report too on a case-study in synthesizingsorting programs.