The initial premise of this paper is that the structure of a proof is inherent in the definition of the proof. Side conditions to deal with the discharging of assumptions means that this does not hold for systems of natural deduction, where proofs are given by monotone inductive definitions. We discuss the idea of using higher order definitions and the notion of a functional closure as a foundation to avoid these problems. In order to focus on structural issues we introduce (...) a more abstract perspective, where a structural proof theory becomes part of a more general theory of functional closures. A notion of proof equations is discussed as a structural classifier and we compare the Russell and Ekman paradoxes to illustrate this. (shrink)

A general definition theory should serve as a foundation for the mathematical study of definitional structures. The central notion of such a theory is a precise explication of the intuitively given notion of a definitional structure. The purpose of this paper is to discuss the proof theory of partial inductive definitions as a foundation for this kind of a more general definition theory. Among the examples discussed is a suggestion for a more abstract definition of lambda-terms (derivations in natural deduction) (...) that could provide a basis for a more systematic definitional approach to general proof theory. (shrink)

This volume contains papers presented at the second international workshop on extensions of logic programming, which was held at the Swedish Institute of Computer Science, Stockhom, January 27-29, 1991. The 12 papers describe and discuss several approaches to extensions of logic programming languages such as PROLOG, as well as connections between logic programming and functional programming, theoretical foundations of extensions, applications, and programming methodologies. The first workshop in this series was held in T}bingen in 1989 and its proceedings areavailable as (...) LNCS 475. The third workshop will be held in Bologna in 1992. (shrink)