𝔖 Bobbio Scriptorium
✦   LIBER   ✦

A Higher-order Interpretation of Deductive Tableau

✍ Scribed by Abdelwaheb Ayari; David Basin

Publisher
Elsevier Science
Year
2001
Tongue
English
Weight
325 KB
Volume
31
Category
Article
ISSN
0747-7171

No coin nor oath required. For personal study only.

✦ Synopsis

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.

📜 SIMILAR VOLUMES

Development of a higher-order ADI-FDTD m
Development of a higher-order ADI-FDTD method
✍ Zhu Wang; Ji Chen; Yinchao Chen 📂 Article 📅 2003 🏛 John Wiley and Sons 🌐 English ⚖ 162 KB

## Abstract In this paper, a higher‐order alternative‐direction‐implicit (ADI) finite‐difference time‐domain (FDTD) method is presented. The dispersion analysis is performed and the results are compared with those derived from the regular ADI‐FDTD method. Based on the dispersion analysis, a guideli

Higher Order Derivatives of a Rational B
Higher Order Derivatives of a Rational Bézier Curve
✍ Guo-Zhao Wang; Guo-Jin Wang 📂 Article 📅 1995 🏛 Elsevier Science 🌐 English ⚖ 212 KB

In this paper, a convenient and effective recurrence formula for the higher order derivatives of a rational degree \(n\) Bézier curve is derived. The \(\operatorname{sth}(s=1,2, \ldots)\)-order derivatives of this curve can be represented as a fraction whose numerator is a vector expression of degre

Positive solutions of a higher order neu
Positive solutions of a higher order neutral differential equation
✍ John R. Graef; Chuanxi Qian; Bo Yang 📂 Article 📅 2003 🏛 John Wiley and Sons 🌐 English ⚖ 120 KB

## Abstract In this paper, we consider the higher order neutral delay differential equation where __p__ : [0, ∞) → (0, ∞) is a continuous function, __r__ > 0 and __σ__ > 0 are constants, and __n__ > 0 is an odd integer. A positive solution __x__(__t__) of Eq. (\*) is called a Class–I solution if _

Best-fit stress performance of a higher-
Best-fit stress performance of a higher-order beam element
✍ Prathap, G. ;Vinayak, R. U. 📂 Article 📅 1996 🏛 John Wiley and Sons 🌐 English ⚖ 394 KB

It is known that finite elements try to capture stresses within each discretized local region in a 'best-fit' sense. In the paper we examine the performance of a beam element based on a higher-order shear deformation theory and show that the best-fit paradigm accounts for the manner in which through