nach oben

1997 | Buch

Kapitel lesen Erstes Kapitel lesen

Logic of Computation

herausgegeben von: Helmut Schwichtenberg

Verlag: Springer Berlin Heidelberg

Buchreihe : NATO ASI Series

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten

Über dieses Buch

The Marktoberdorf Summer School 1995 'Logic of Computation' was the 16th in a series of Advanced Study Institutes under the sponsorship of the NATO Scientific Affairs Division held in Marktoberdorf. Its scientific goal was to survey recent progress on the impact of logical methods in software development. The courses dealt with many different aspects of this interplay, where major progress has been made. Of particular importance were the following. • The proofs-as-programs paradigm, which makes it possible to extract verified programs directly from proofs. Here a higher order logic or type theoretic setup of the underlying language has developed into a standard. • Extensions of logic programming, e.g. by allowing more general formulas and/or higher order languages. • Proof theoretic methods, which provide tools to deal with questions of feasibility of computations and also to develop a general mathematical understanding of complexity questions. • Rewrite systems and unification, again in a higher order context. Closely related is the now well-established Grabner basis theory, which recently has found interesting applications. • Category theoretic and more generally algebraic methods and techniques to analyze the semantics of programming languages. All these issues were covered by a team of leading researchers. Their courses were grouped under the following headings.

Inhaltsverzeichnis

Frontmatter

Lectures on Semantics: The Initial Algebra and Final Coalgebra Perspectives

Abstract

These lectures give a non-standard introduction, for computer science students, to the mathematical semantics of formal languages. We do not attempt to give a balanced treatment, but instead focus on some key general ideas, illustrated with simple examples. The ideas are formulated using some elementary category theoretic notions. All the required category theory is introduced in the lectures. In addition to the familiar initial algebra approach to syntax and semantics we examine the less familiar final coalgebra approach to operational semantics. Our treatment of formal semantics is intended to complement a more standard introduction.

Peter Aczel

Introduction to Groebner Bases

Abstract

A comprehensive treatment of Groebner bases theory is far beyond what can be done in four lectures. Recent text books on Groebner bases like (Becker, Weispfenning 1993) and (Cox, Little, O’Shea 1992) present the material on several hundred pages. However, there are only a few key ideas behind Groebner bases theory. It is the objective of these four lectures to explain these ideas as simply as possible and to give an overview of the applications.

Bruno Buchberger

Bounded Arithmetic and Propositional Proof Complexity

Abstract

This is a survey of basic facts about bounded arithmetic and about the relationships between bounded arithmetic and propositional proof complexity. We introduce the theories and of bounded arithmetic and characterize their proof theoretic strength and their provably total functions in terms of the polynomial time hierarchy. We discuss other axiomatizations of bounded arithmetic, such as minimization axioms. It is shown that the bounded arithmetic hierarchy collapses if and only if bounded arithmetic proves that the polynomial hierarchy collapses.

We discuss Frege and extended Frege proof length, and the two translations from bounded arithmetic proofs into propositional proofs. We present some theorems on bounding the lengths of propositional interpolants in terms of cut-free proof length and in terms of the lengths of resolution refutations. We then define the Razborov-Rudich notion of natural proofs of P ≠ NP and discuss Razborov’s theorem that certain fragments of bounded arithmetic cannot prove superpolynomial lower bounds on circuit size, assuming a strong cryptographic conjecture. Finally, a complete presentation of a proof of the theorem of Razborov is given.

Samuel R. Buss

The Structure of Nuprl’s Type Theory

Abstract

After my lectures on this topic were delivered in July 1995 at Markt ob erdorf, my colleagues and I made available much more related material both at the Nuprl home page on the World Wide Web (“the Web”) (www.cs.cornell.edu/Info/NuPrl/nuprl.html) and in publications [22], some soon to appear [11].

Robert L. Constable

Axiomatisations, Proofs, and Formal Specifications of Algorithms: Commented Case Studies in the Coq Proof Assistant

Abstract

Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications. It may be obtained by anonymous FTP from site ftp.inria.fr, directory INRIA/coq/Vo. 10. We shall not discuss here in detail how to make proofs in Coq, and refer the interested reader to the Coq Tutorial, in the documentation section of the standard distribution. We shall concentrate in the following lessons on axiomatisations and specifications in the Gallina specification language.

Gérard Huet

Some Proof Theory of First Order Logic Programming

Abstract

This article presents some basic aspects of the proof theory of first order logic programming. We start off from general resolution, unit resolution, input resolution and SLD resolution. Then we turn to the sequent calculus and its relationship to resolution and present deductive systems for logic programs (with negation). After discussing partiality in logic programming, this article ends with the introduction of inductive extensions of logic programs, which provide a powerful proof-theoretic framework for logic programming.

Gerhard Jäger

Timed Rewriting Logic for the Specification of Time-Sensitive Systems

Abstract

In this paper Timed Rewriting Logic and its extension Timed Rewriting Logic with Delays are presented.

Timed Rewriting Logic is an extension of Meseguer’s Rewriting Logic. The dynamic behaviour of a time dependent system is described by nondeterministic term rewriting where each rewriting step is labeled by a time stamp. The functional and the static properties of a system are described by algebraic specifications. Deduction rules for timed behaviour and a model class semantics are given. The existence of initial models and the decidability of ground finite timed rewriting systems is proven.

Timed Rewriting Logic with Delays is used for modeling imprecise real-time constraints. Here the labels of the rewrite steps are time intervals instead of time stamps. The deduction rules and the model class semantics are generalizations of the corresponding notions for Timed Rewriting Logic. The results concerning existence of initial models and decidability of Timed Rewriting Logic specifications are extended to Timed Rewriting Logic with Delays.

The approach is illustrated by several examples, such as clocks, time out, timer, and an imprecise oscillator. As the main application we show how Timed Rewriting Logic with Delays can be used to specify clocks with a drift, clocks in a distributed system and Timed Automata.

Piotr Kosiuczenko, Martin Wirsing

Logic Programming and Meta-Logic

Abstract

The theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logic programming languages. Two such languages, lambda Prolog and its linear logic refinement, Lolli, provide for various forms of abstraction (modules, abstract data types, and higher-order programming) but lack primitives for concurrency. The logic programming language LO (Linear Objects) provides some primitives for concurrency but lacks abstraction mechanisms. A logic programming presentation of all of higher-order linear logic, named Forum, modularly extends these other languages and also allows for abstractions and concurrency in specifications. To illustrate the expressive strengths of Forum, we specify in it a sequent calculus proof system and the operational semantics of a programming language that incorporates side-effects.

Dale Miller

Proofs, Lambda Terms and Control Operators

Abstract

The so-called continuation-passing-style translation (cps-translation) has been introduced by Fischer [8] for the λ-calculus and extended to the λ-calculus with control operators C and A by Felleisen et al. in [7]. By giving a typing a connection with implicational propositional logic has been established by Meyer and Wand [13] for the λ-calculus and extended to the λ-calculus with control operators C and A by Griffin [10]. Griffin has shown that all evaluations with respect to call-by-value β-conversion and the standard conversion rules for C and A terminate. More precisely Griffin extends the Meyer/Wand typing of Fischers cps-translation M of a term M to the language involving the control operators C and A. It still holds that if M has type A, then M has type A°, where A° is defined as P°:=P and (A → B)°:= A° → B° → F (which is equivalent to B° →A°). Griffin’s proof of termination of evaluation is based on Plotkin’s [16] technique of the so-called colon-translation (denoted M:V and typed by M ^A:V ^A°) and context unwrapping (denoted V ^E and typed by requiring V to be of type B° and the evaluation context E to be of type B with the ‘hole’ of type A).

Helmut Schwichtenberg

Basic Proof Theory with Applications to Computation

Abstract

These lecture notes extend and revise an earlier joint paper: Wainer and Wallen (1992). The intension is to introduce some of the most fundamental concepts and results of proof theory, and to illustrate their relevance to the theory of computation.Each lecture contains one main theorem, given in its simplest and most basic form. The aim is to convey the essential ideas behinf their proofs, keeping the syntactic detail to a minimum so as not to obscure their underlying structure. Some of these results are use elsewhere in this volume, sometimes implicitly and sometimes explicitly, but often in more sophisticated forms. As with car sales, the hope is that once having driven the basic version, the reader will quickly appreciate the more streamlined models.

Stanley S. Wainer

Backmatter

Titel: Logic of Computation
herausgegeben von: Helmut Schwichtenberg
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-59048-1
Print ISBN: 978-3-642-63832-9
DOI: https://doi.org/10.1007/978-3-642-59048-1

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Lectures on Semantics: The Initial Algebra and Final Coalgebra Perspectives

Introduction to Groebner Bases

Bounded Arithmetic and Propositional Proof Complexity

The Structure of Nuprl’s Type Theory

Axiomatisations, Proofs, and Formal Specifications of Algorithms: Commented Case Studies in the Coq Proof Assistant

Some Proof Theory of First Order Logic Programming

Timed Rewriting Logic for the Specification of Time-Sensitive Systems

Logic Programming and Meta-Logic

Proofs, Lambda Terms and Control Operators

Basic Proof Theory with Applications to Computation

Backmatter