A Higher-order Interpretation of Deductive Tableau

摘要

The deductive Tableau of Manna and Waldinger is a formal system with an associ- ated 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 synthe- sis methodology can be applied in our setting as well as new methodologies that take advantage of these higher-order features.