Publications: Journal Article: A Higher-order Interpretation of Deductive Tableau

Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

Options:

Goto entry point

Author, Editor(s)

Author(s):

Ayari, Abdelwaheb
Basin, David A.

dblp
dblp

BibTeX cite key*:

AyariBasin2001

Title

Title*:

A Higher-order Interpretation of Deductive Tableau

Journal

Journal Title*:	Journal of Symbolic Computation	Journal's URL:	http://www.academicpress.com/jsc
Download URL for the article:		Language:	English

Publisher

Publisher's Name:		Publisher's URL:
Publisher's Address:		ISSN:

Vol, No, pp, Date

Volume*:	31	Number:	5
Publishing Date:	May 2001
Pages*:	487-520	Number of VG Pages:
Page Start:		Page End:
Sequence Number:		DOI:

Note:
(LaTeX) 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.
URL for the Abstract:
Categories, Keywords:
HyperLinks / References / URLs:
Copyright Message:
Personal Comments:
Download Access Level:

Correlation

MPG Unit:	Max-Planck-Institut für Informatik

MPG Subunit:	Programming Logics Group
Audience:	experts only
Appearance:	MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat

BibTeX Entry:

@ARTICLE{AyariBasin2001,
AUTHOR = {Ayari, Abdelwaheb and Basin, David A.},
TITLE = {A Higher-order Interpretation of Deductive Tableau},
JOURNAL = {Journal of Symbolic Computation},
YEAR = {2001},
NUMBER = {5},
VOLUME = {31},
PAGES = {487--520},
MONTH = {May},
}

Entry last modified by Uwe Brahm, 03/12/2010

Edit History (please click the blue arrow to see the details)

	Editor(s) Christine Kiesel	Created 08/21/2001 10:47:54 AM
Revisions 2. 1. 0.	Editor(s) Uwe Brahm Christine Kiesel Christine Kiesel	Edit Dates 03/28/2002 12:43:11 AM 21.08.2001 10:55:41 AM 21.08.2001 10:54:40 AM