Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

A Higher-order Interpretation of Deductive Tableau

MPG-Autoren
/persons/resource/persons44047

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

/persons/resource/persons44075

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

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


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